attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";

--- a/src/Pure/Isar/method.ML	Fri Aug 22 15:39:30 2014 +0200
+++ b/src/Pure/Isar/method.ML	Fri Aug 22 15:55:24 2014 +0200
@@ -474,8 +474,8 @@
             | _ =>
                 let
                   val facts =
-                    Attrib.partial_evaluation ctxt
-                      [((Binding.empty, [Attrib.internal (K att)]), thms)];
+                    Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
+                    |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K att)]), bs));
                   fun decl phi =
                     Context.mapping I init #>
                     Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;