diff -r 2e22cdccdc38 -r 358b6020f8b6 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Mon Dec 10 10:41:29 2012 +0100 +++ b/src/HOL/Tools/try0.ML Mon Dec 10 13:52:33 2012 +0100 @@ -138,7 +138,7 @@ Auto_Try => "Auto Try Methods found a proof" | Try => "Try Methods found a proof" | Normal => "Try this") ^ ": " ^ - Sendback.markup + Active.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"