src/Pure/sign.ML
changeset 24485 687bbb686ef9
parent 24370 757b093e3459
child 24517 eaed6ac5f7f2
     1.1 --- a/src/Pure/sign.ML	Thu Aug 30 15:04:42 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Aug 30 15:04:44 2007 +0200
     1.3 @@ -567,9 +567,10 @@
     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  
     1.9 -    fun infer args = TypeInfer.infer_types pp (tsig_of thy)
    1.10 -        Type.mode_default (try (Consts.the_constraint consts)) def_type used freeze args |>> map fst
    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
    1.13        handle TYPE (msg, _, _) => error msg;
    1.14  
    1.15      fun check T t = Exn.Result (singleton (fst o infer) (t, T))