diff -r de3fd08bb41c -r d4380e9b287b src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Thu Aug 30 21:44:29 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Thu Aug 30 22:35:34 2007 +0200
@@ -238,7 +238,7 @@
   vt0 holds the initial sort constraints, from the conjecture clauses.*)
 fun clause_of_strees ctxt vt0 ts =
   let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in
-    singleton (ProofContext.infer_types ctxt) (TypeInfer.constrain (fix_sorts vt dt) HOLogic.boolT)
+    singleton (Syntax.check_terms ctxt) (TypeInfer.constrain (fix_sorts vt dt) HOLogic.boolT)
   end;
 
 (*Quantification over a list of Vars. FIXME: for term.ML??*)