--- a/src/HOL/Tools/res_reconstruct.ML Mon Oct 13 14:04:28 2008 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Mon Oct 13 14:04:29 2008 +0200
@@ -344,7 +344,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 = Syntax.string_of_term ctxt
+ let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term)
val _ = trace ("\n\nisar_lines: start\n")
fun doline have (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*)
(case permuted_clause t ctms of