changeset 63518 | ae8fd6fe63a1 |
parent 62984 | 61b32a6d87e9 |
child 63690 | 48a2c88091d7 |
--- a/src/HOL/Tools/try0.ML Sat Jul 16 18:56:43 2016 +0200 +++ b/src/HOL/Tools/try0.ML Sat Jul 16 19:35:27 2016 +0200 @@ -143,7 +143,7 @@ Auto_Try => "Auto Try0 found a proof" | Try => "Try0 found a proof" | Normal => "Try this") ^ ": " ^ - Active.sendback_markup [Markup.padding_command] + Active.sendback_markup_command ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^ " " ^ command) ^ (case xs of