# HG changeset patch
# User wenzelm
# Date 1408715724 -7200
# Node ID 07b5373955db39134d3f4417017a785ac3eec239
# Parent  154ae20ead351b6711e6bc7cd3038b146f89dd06
attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";

diff -r 154ae20ead35 -r 07b5373955db src/Pure/Isar/method.ML
--- 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;