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.
proper Sendback.markup, as required for standard Prover IDE protocol (see also c62ce309dc26);
authorwenzelm
Thu, 06 Dec 2012 23:01:49 +0100
changeset 50410 6ab3fadf43af
parent 50409 5eaebd8e52f4
child 50413 bf01be7d1a44
proper Sendback.markup, as required for standard Prover IDE protocol (see also c62ce309dc26);
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Dec 06 22:12:25 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Dec 06 23:01:49 2012 +0100
@@ -728,7 +728,7 @@
           in
             "\n\nStructured proof "
               ^ (commas msg |> not (null msg) ? enclose "(" ")")
-              ^ ":\n" ^ Markup.markup Markup.sendback isar_text
+              ^ ":\n" ^ Sendback.markup isar_text
           end
       end
     val isar_proof =
isabelle