# HG changeset patch
# User wenzelm
# Date 1354831309 -3600
# Node ID 6ab3fadf43af3b6a1dfb7d9a72da873562110d34
# Parent  5eaebd8e52f4f5dd5f93682819c3580d12228fc9
proper Sendback.markup, as required for standard Prover IDE protocol (see also c62ce309dc26);

diff -r 5eaebd8e52f4 -r 6ab3fadf43af src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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 =