diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -352,7 +352,7 @@
 (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
   ATP may have their literals reordered.*)
 fun isar_lines ctxt ctms =
-  let val string_of = ProofContext.string_of_term ctxt
+  let val string_of = Syntax.string_of_term ctxt
       fun doline have (lname, t, []) =  (*No deps: it's a conjecture clause, with no proof.*)
            (case permuted_clause t ctms of
                 SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"