diff -r 290454649b8c -r 1e057a3f087d src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Sun Apr 15 14:31:47 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Sun Apr 15 14:31:49 2007 +0200
@@ -282,12 +282,7 @@
   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
-      val infer = Sign.infer_types (ProofContext.pp ctxt) (ProofContext.theory_of ctxt)
-                      (ProofContext.consts_of ctxt) (Variable.def_type ctxt false)
-                      (Variable.def_sort ctxt) (Variable.names_of ctxt) true
-  in 
-     #1(infer ([fix_sorts vt dt], HOLogic.boolT))
-  end; 
+  in #1 (singleton (ProofContext.infer_types ctxt) (fix_sorts vt dt, HOLogic.boolT)) end;
 
 (*Quantification over a list of Vars. FUXNE: for term.ML??*)
 fun list_all_var ([], t: term) = t