--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Nov 22 12:22:03 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Nov 22 13:21:02 2012 +0100
@@ -233,15 +233,14 @@
command_call (string_for_reconstructor reconstr) ss
fun try_command_line banner time command =
- banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^
- show_time time ^ "."
+ banner ^ ": " ^ Sendback.markup command ^ show_time time ^ "."
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
case minimize_command ss of
"" => ""
| command =>
- "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
+ "\nTo minimize: " ^ Sendback.markup command ^ "."
fun split_used_facts facts =
facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
@@ -1055,7 +1054,7 @@
else if preplay then
" (" ^ string_from_ext_time ext_time ^ ")"
else
- "") ^ ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text
+ "") ^ ":\n" ^ Sendback.markup isar_text
end
val isar_proof =
if debug then