Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;
authorwenzelm
Sat, 01 Sep 2007 18:17:42 +0200
changeset 24517 eaed6ac5f7f2
parent 24516 c121834a8808
child 24518 4dd086997bab
read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;
src/Pure/sign.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle