# HG changeset patch
# User wenzelm
# Date 1188663462 -7200
# Node ID eaed6ac5f7f25fce690f2d3efdf595839e236691
# Parent  c121834a8808b61821ffc7bf9b4e54b01d95d393
read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;

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