simplified ProofContext.infer_types(_pats);

--- a/TFL/tfl.ML	Wed Apr 18 16:23:31 2007 +0200
+++ b/TFL/tfl.ML	Wed Apr 18 21:30:14 2007 +0200
@@ -367,8 +367,8 @@
 
 (*For Isabelle, the lhs of a definition must be a constant.*)
 fun mk_const_def sign (c, Ty, rhs) =
-  #1 (singleton (ProofContext.infer_types (ProofContext.init sign))
-    (Const("==",dummyT) $ Const(Sign.full_name sign c,Ty) $ rhs, propT));
+  singleton (ProofContext.infer_types (ProofContext.init sign))
+    (Const("==",dummyT) $ Const(Sign.full_name sign c,Ty) $ rhs);
 
 (*Make all TVars available for instantiation by adding a ? to the front*)
 fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)

--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Apr 18 16:23:31 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Apr 18 21:30:14 2007 +0200
@@ -209,7 +209,7 @@
     val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
     val def_prop as _ $ _ $ t =
       singleton (ProofContext.infer_types (ProofContext.init thy))
-        (Logic.mk_equals (Const (fname, dummyT), rhs), propT) |> #1;
+        (Logic.mk_equals (Const (fname, dummyT), rhs));
   in ((def_name, def_prop), subst_bounds (rev (map Free frees), strip_abs_body t)) end;
 
 

--- a/src/HOL/Tools/primrec_package.ML	Wed Apr 18 16:23:31 2007 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Wed Apr 18 21:30:14 2007 +0200
@@ -204,7 +204,7 @@
     val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
     val def_prop =
       singleton (ProofContext.infer_types (ProofContext.init thy))
-        (Logic.mk_equals (Const (fname, dummyT), rhs), propT) |> #1;
+        (Logic.mk_equals (Const (fname, dummyT), rhs));
   in (def_name, def_prop) end;
 
 

--- a/src/HOL/Tools/res_reconstruct.ML	Wed Apr 18 16:23:31 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Wed Apr 18 21:30:14 2007 +0200
@@ -281,8 +281,9 @@
 (*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
   vt0 holds the initial sort constraints, from the conjecture clauses.*)
 fun clause_of_strees_aux ctxt vt0 ts = 
-  let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts
-  in #1 (singleton (ProofContext.infer_types ctxt) (fix_sorts vt dt, HOLogic.boolT)) end;
+  let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in
+    singleton (ProofContext.infer_types ctxt) (TypeInfer.constrain (fix_sorts vt dt) HOLogic.boolT)
+  end;
 
 (*Quantification over a list of Vars. FUXNE: for term.ML??*)
 fun list_all_var ([], t: term) = t

--- a/src/HOLCF/fixrec_package.ML	Wed Apr 18 16:23:31 2007 +0200
+++ b/src/HOLCF/fixrec_package.ML	Wed Apr 18 21:30:14 2007 +0200
@@ -20,11 +20,10 @@
 
 (* legacy type inference *)
 
-fun legacy_infer_types thy (t, T) =
-  #1 (singleton (ProofContext.infer_types (ProofContext.init thy)) (Sign.intern_term thy t, T));
+fun legacy_infer_term thy t =
+  singleton (ProofContext.infer_types (ProofContext.init thy)) (Sign.intern_term thy t);
 
-fun legacy_infer_term thy t = legacy_infer_types thy (t, dummyT);
-fun legacy_infer_prop thy t = legacy_infer_types thy (t, propT);
+fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain t propT);
 
 
 val fix_eq2 = thm "fix_eq2";

--- a/src/Pure/Isar/proof_context.ML	Wed Apr 18 16:23:31 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 18 21:30:14 2007 +0200
@@ -67,8 +67,8 @@
   val cert_prop: Proof.context -> term -> term
   val cert_term_pats: typ -> Proof.context -> term list -> term list
   val cert_prop_pats: Proof.context -> term list -> term list
-  val infer_types: Proof.context -> (term * typ) list -> (term * typ) list
-  val infer_types_pat: Proof.context -> (term * typ) list -> (term * typ) list
+  val infer_types: Proof.context -> term list -> term list
+  val infer_types_pats: Proof.context -> term list -> term list
   val infer_type: Proof.context -> string -> typ
   val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
@@ -563,14 +563,15 @@
 
 local
 
-fun gen_infer_types pattern ctxt =
+fun gen_infer_types pattern ctxt ts =
   TypeInfer.infer_types (pp ctxt) (tsig_of ctxt) (try (Consts.the_constraint (consts_of ctxt)))
-    (Variable.def_type ctxt pattern) (Variable.names_of ctxt) (not pattern) #> #1;
+    (Variable.def_type ctxt pattern) (Variable.names_of ctxt) (not pattern) (map (rpair dummyT) ts)
+  |> #1 |> map #1;
 
 in
 
 val infer_types = gen_infer_types false;
-val infer_types_pat = gen_infer_types true;
+val infer_types_pats = gen_infer_types true;
 
 end;
 
@@ -578,7 +579,7 @@
 (* inferred types of parameters *)
 
 fun infer_type ctxt x =
-  #2 (singleton (infer_types ctxt) (Free (x, dummyT), dummyT));
+  Term.fastype_of (singleton (infer_types ctxt) (Free (x, dummyT)));
 
 fun inferred_param x ctxt =
   let val T = infer_type ctxt x

--- a/src/Pure/Tools/nbe.ML	Wed Apr 18 16:23:31 2007 +0200
+++ b/src/Pure/Tools/nbe.ML	Wed Apr 18 21:30:14 2007 +0200
@@ -148,8 +148,8 @@
       error ("Illegal schematic type variables in normalized term: "
         ^ setmp show_types true (Sign.string_of_term thy) t);
     val ty = type_of t;
-    fun constrain t =          (* FIXME really pat? *)
-      #1 (singleton (ProofContext.infer_types_pat (ProofContext.init thy)) (t, ty));
+    fun constrain t =
+      singleton (ProofContext.infer_types (ProofContext.init thy)) (TypeInfer.constrain t ty);
     val _ = ensure_funs thy funcgr t;
   in
     t