[racket-dev] Am I misusing judgment-holds ?

I want to use judgment-holds in a side-condition but sometimes it
doesn't quite work because it's a macro. In the following example,
judgment-holds does not use the value bound to tau. Is there a nice
way to make it do what I want?

#lang racket
(require redex)

(define-language L
  (e integer true false)
  (τ bool int))

(define-judgment-form L
  #:mode (⊢ I O)
  #:contract (⊢ e τ)
  [(⊢ integer int)]
  [(⊢ true bool)]
  [(⊢ true bool)])

(define-metafunction L
  [(type-checks? e τ)
   ,(judgment-holds (⊢ e τ))
   (side-condition (printf "τ = ~a\n" (term τ)))])


Welcome to DrRacket, version 5.3.0.20 [3m].
Language: racket [custom].
> (judgment-holds (⊢ 1 int))
#t
> (judgment-holds (⊢ 1 bool))
#f
> (term (type-checks? 1 int))
τ = int
#t
> (term (type-checks? 1 bool))
τ = bool
#t