# HG changeset patch
# User blanchet
# Date 1283282239 -7200
# Node ID da5e4f182f69c51ec6750af1776a3516de4343e3
# Parent  53a9563fa2212dfad5309e5f24f0f9f4e93058d3
distinguish between "by" and "apply"

diff -r 53a9563fa221 -r da5e4f182f69 src/HOL/Tools/try.ML
--- 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"