read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;
authorwenzelm
Sat Sep 01 18:17:42 2007 +0200 (2007-09-01)
changeset 24517eaed6ac5f7f2
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
     1.1 --- a/src/Pure/sign.ML	Sat Sep 01 18:17:40 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Sat Sep 01 18:17:42 2007 +0200
     1.3 @@ -567,7 +567,8 @@
     1.4      pp is_logtype syn consts map_free ctxt (def_type, def_sort) used freeze raw_args =
     1.5    let
     1.6      val thy = ProofContext.theory_of ctxt;
     1.7 -    val check_typs = Syntax.check_typs (Type.set_mode Type.mode_default ctxt);
     1.8 +    fun check_typs Ts = map (certify_typ thy) Ts
     1.9 +      handle TYPE (msg, _, _) => error msg;
    1.10  
    1.11      fun infer args = TypeInfer.infer_types pp (tsig_of thy) check_typs
    1.12          (try (Consts.the_constraint consts)) def_type used freeze args |>> map fst