src/ZF/Tools/datatype_package.ML

   (*** Prove the case theorems ***)
 
   (*Each equation has the form
     case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
   fun mk_case_eqn (((_,T,_), name, args, _), case_free) =
-    FOLogic.mk_Trueprop
+    \<^make_judgment>
       (FOLogic.mk_eq
        (case_tm $
          (list_comb (Const (Sign.intern_const thy1 name,T),
                      args)),
         list_comb (case_free, args)));

         (*Each equation has the form
           REC(coni(args)) = f_coni(args, REC(rec_arg), ...)
           where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive
           constructor argument.*)
         fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) =
-          FOLogic.mk_Trueprop
+          \<^make_judgment>
            (FOLogic.mk_eq
             (recursor_tm $
              (list_comb (Const (Sign.intern_const thy2 name,T),
                          args)),
              subst_rec (Term.betapplys (recursor_case, args))));