# HG changeset patch
# User wenzelm
# Date 1321913011 -3600
# Node ID a3ed5b65b85ef7269769962d1b7afd706112f716
# Parent  8e71b9228d2d47164b6d5d8189d438d02a1c7132
drop vacuous decls;

diff -r 8e71b9228d2d -r a3ed5b65b85e src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Nov 21 21:38:08 2011 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Nov 21 23:03:31 2011 +0100
@@ -281,6 +281,7 @@
         val facts' =
           if eq_list (eq_fst strict_eq_thm) (decls', fact') then
             [((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')]
+          else if forall (null o snd) decls' then [((b, []), fact')]
           else [(empty_binding, decls'), ((b, []), fact')];
       in (facts', context') end)
   |> fst |> flat |> map (apsnd (map (apfst single)));