# HG changeset patch
# User wenzelm
# Date 1223899469 -7200
# Node ID 78ac28f80a1cfc8a30271f1373f95ef83875e685
# Parent  47d88239658d65c4ce176de9479c1644e4d3800a
** Update from Fabian **
reset print mode when producing proof text;

diff -r 47d88239658d -r 78ac28f80a1c src/HOL/Tools/res_reconstruct.ML
--- 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