Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
changeset 50410 6ab3fadf43af
parent 50277 e0a4d8404c76
child 50450 358b6020f8b6 
--- 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