changeset 50163 | c62ce309dc26 |
parent 49866 | 619acbd72664 |
child 50201 | c26369c9eda6 |
--- a/src/HOL/Tools/try0.ML Thu Nov 22 12:22:03 2012 +0100 +++ b/src/HOL/Tools/try0.ML Thu Nov 22 13:21:02 2012 +0100 @@ -138,7 +138,7 @@ Auto_Try => "Auto Try Methods found a proof" | Try => "Try Methods found a proof" | Normal => "Try this") ^ ": " ^ - Markup.markup Isabelle_Markup.sendback + Sendback.markup ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^ "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"