simplified TypeInfer.infer_types;

--- a/src/Pure/Isar/proof_context.ML	Wed Jun 18 22:32:02 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jun 18 22:32:03 2008 +0200
@@ -579,8 +579,7 @@
   let val Mode {pattern, ...} = get_mode ctxt in
     TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
       (try (Consts.the_constraint (consts_of ctxt))) (Variable.def_type ctxt pattern)
-      (Variable.names_of ctxt) (Variable.maxidx_of ctxt) NONE (map (rpair dummyT) ts)
-    |> #1 |> map #1
+      (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
     handle TYPE (msg, _, _) => error msg
   end;
 

--- a/src/Tools/nbe.ML	Wed Jun 18 22:32:02 2008 +0200
+++ b/src/Tools/nbe.ML	Wed Jun 18 22:32:03 2008 +0200
@@ -385,11 +385,10 @@
       (map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t []));
     val type_frees = Term.map_aterms
       (fn (t as Term.Free (s, _)) => the_default t (type_free s) | t => t);
-    fun type_infer t = [(t, ty)]
-      |> TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
-           (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE)
-           Name.context 0 NONE
-      |> fst |> the_single |> fst;
+    fun type_infer t =
+      singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
+        (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
+      (TypeInfer.constrain ty t);
     fun check_tvars t = if null (Term.term_tvars t) then t else
       error ("Illegal schematic type variables in normalized term: "
         ^ setmp show_types true (Syntax.string_of_term_global thy) t);