Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
** Update from Fabian **
authorwenzelm
Mon, 13 Oct 2008 14:04:29 +0200
changeset 28572 78ac28f80a1c
parent 28571 47d88239658d
child 28573 6403f0e16269
** Update from Fabian ** reset print mode when producing proof text;
src/HOL/Tools/res_reconstruct.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle