Fixes define-judgment-form at the top-level with errortrace enabled

collects/redex/private/reduction-semantics.rkt

@@ -1495,8 +1495,7 @@
          (define nts (definition-nts lang stx syn-err-name))
          (define-values (judgment-form-name dup-form-names mode position-contracts clauses)
            (parse-define-judgment-form-body #'body syn-err-name stx))
-         (syntax-property
+         (define definitions
-          (prune-syntax
            #`(begin
                (define-syntax #,judgment-form-name 
                  (judgment-form '#,judgment-form-name '#,mode #'judgment-form-proc #'#,lang #'judgment-form-lws))
@@ -1517,6 +1516,15 @@
                                    [(_ clauses)
                                     (compile-judgment-form-lws (syntax->list #'clauses))]))])
                    (delayed #,clauses)))))
+         (syntax-property
+          (prune-syntax
+           (if (eq? 'top-level (syntax-local-context))
+               ; Introduce the names before using them, to allow
+               ; judgment form definition at the top-level.
+               #`(begin 
+                   (define-syntaxes (judgment-form-proc judgment-form-lws) (values))
+                   #,definitions)
+               definitions))
           'disappeared-use
           (map syntax-local-introduce dup-form-names)))]))
   

collects/redex/tests/tl-test.rkt

@@ -2024,6 +2024,17 @@
                                   
                                   })))
     
+    (parameterize ([current-namespace (make-base-namespace)])
+      (eval '(require errortrace))
+      (eval '(require redex/reduction-semantics))
+      (eval '(define-language L))
+      (eval '(define-judgment-form L
+               mode : I
+               [(J a)
+                (J b)]
+               [(J b)]))
+      (test (eval '(judgment-holds (J a))) #t))
+    
     (parameterize ([current-namespace (make-base-namespace)])
       (eval '(require redex/reduction-semantics))
       (eval '(define-language L