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 =