diff -r c121834a8808 -r eaed6ac5f7f2 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Sep 01 18:17:40 2007 +0200
+++ b/src/Pure/sign.ML	Sat Sep 01 18:17:42 2007 +0200
@@ -567,7 +567,8 @@
     pp is_logtype syn consts map_free ctxt (def_type, def_sort) used freeze raw_args =
   let
     val thy = ProofContext.theory_of ctxt;
-    val check_typs = Syntax.check_typs (Type.set_mode Type.mode_default ctxt);
+    fun check_typs Ts = map (certify_typ thy) Ts
+      handle TYPE (msg, _, _) => error msg;
 
     fun infer args = TypeInfer.infer_types pp (tsig_of thy) check_typs
         (try (Consts.the_constraint consts)) def_type used freeze args |>> map fst