--- 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"