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_isar.ML
changeset 63518 ae8fd6fe63a1
parent 62826 eb94e570c1a4
child 63692 1bc4bc2c9fd1 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jul 16 19:35:27 2016 +0200
@@ -441,7 +441,7 @@
               in
                 one_line_proof_text ctxt 0 one_line_params ^
                 "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
-                Active.sendback_markup [Markup.padding_command]
+                Active.sendback_markup_command
                   (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
               end)
           end
isabelle