src/Tools/nbe.ML
changeset 39288 f1ae2493d93f
parent 39134 917b4b6ba3d2
child 39290 44e4d8dfd6bf
     1.1 --- a/src/Tools/nbe.ML	Sun Sep 12 17:39:02 2010 +0200
     1.2 +++ b/src/Tools/nbe.ML	Sun Sep 12 19:04:02 2010 +0200
     1.3 @@ -551,7 +551,7 @@
     1.4      fun type_infer t =
     1.5        singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
     1.6          (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
     1.7 -      (Type_Infer.constrain ty' t);
     1.8 +      (Type.constraint ty' t);
     1.9      val string_of_term =
    1.10        Syntax.string_of_term (Config.put show_types true (Syntax.init_pretty_global thy));
    1.11      fun check_tvars t =