src/Tools/nbe.ML
changeset 27264 843472ae2116
parent 27103 d8549f4d900b
child 27499 150558266831
     1.1 --- a/src/Tools/nbe.ML	Wed Jun 18 22:32:02 2008 +0200
     1.2 +++ b/src/Tools/nbe.ML	Wed Jun 18 22:32:03 2008 +0200
     1.3 @@ -385,11 +385,10 @@
     1.4        (map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t []));
     1.5      val type_frees = Term.map_aterms
     1.6        (fn (t as Term.Free (s, _)) => the_default t (type_free s) | t => t);
     1.7 -    fun type_infer t = [(t, ty)]
     1.8 -      |> TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
     1.9 -           (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE)
    1.10 -           Name.context 0 NONE
    1.11 -      |> fst |> the_single |> fst;
    1.12 +    fun type_infer t =
    1.13 +      singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
    1.14 +        (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
    1.15 +      (TypeInfer.constrain ty t);
    1.16      fun check_tvars t = if null (Term.term_tvars t) then t else
    1.17        error ("Illegal schematic type variables in normalized term: "
    1.18          ^ setmp show_types true (Syntax.string_of_term_global thy) t);