src/Tools/nbe.ML
changeset 42405 13ecdb3057d8
parent 42361 23f352990944
child 43323 28e71a685c84
     1.1 --- a/src/Tools/nbe.ML	Tue Apr 19 16:13:04 2011 +0200
     1.2 +++ b/src/Tools/nbe.ML	Tue Apr 19 20:47:02 2011 +0200
     1.3 @@ -545,9 +545,9 @@
     1.4      val ctxt = Syntax.init_pretty_global thy;
     1.5      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
     1.6      val ty' = typ_of_itype program vs0 ty;
     1.7 -    fun type_infer t = singleton
     1.8 -      (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
     1.9 -      (Type.constraint ty' t);
    1.10 +    fun type_infer t =
    1.11 +      Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
    1.12 +        (Type.constraint ty' t);
    1.13      fun check_tvars t =
    1.14        if null (Term.add_tvars t []) then t
    1.15        else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);