# HG changeset patch
# User blanchet
# Date 1343311696 -7200
# Node ID 619531d87ce4c5471ffc6c33c015f7524bd4089d
# Parent  2307efbfc554d87a3be1b70796058ab60f8e2d12
[1] goes after any attributes

diff -r 2307efbfc554 -r 619531d87ce4 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Jul 26 11:08:16 2012 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Jul 26 16:08:16 2012 +0200
@@ -77,12 +77,13 @@
   if mode <> Auto_Try orelse run_if_auto_try then
     let val attrs = attrs_text attrs quad in
       do_generic timeout_opt
-                 (name ^ (if all_goals andalso
-                             nprems_of (#goal (Proof.goal st)) > 1 then
-                            "[1]"
-                          else
-                            "") ^
-                  attrs) I (#goal o Proof.goal)
+                 (name ^ attrs ^
+                  (if all_goals andalso
+                      nprems_of (#goal (Proof.goal st)) > 1 then
+                     " [1]"
+                   else
+                     ""))
+                 I (#goal o Proof.goal)
                  (apply_named_method_on_first_goal (name ^ attrs)
                                                    (Proof.theory_of st)) st
     end