--- a/src/HOL/Tools/try.ML Tue Aug 31 21:02:07 2010 +0200
+++ b/src/HOL/Tools/try.ML Tue Aug 31 21:17:19 2010 +0200
@@ -66,8 +66,10 @@
[] => writeln "No proof found."
| xs as (s, _) :: _ =>
priority ("Try this command: " ^
- Markup.markup Markup.sendback ("apply " ^ s) ^ ".\n" ^
- "(" ^ space_implode "; " (map time_string xs) ^ ")\n")
+ Markup.markup Markup.sendback
+ ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
+ " " ^ s) ^
+ ".\n(" ^ space_implode "; " (map time_string xs) ^ ")\n")
val tryN = "try"