drop vacuous decls;
authorwenzelm
Mon Nov 21 23:03:31 2011 +0100 (2011-11-21)
changeset 45612a3ed5b65b85e
parent 45611 8e71b9228d2d
child 45613 70e5b43535cd
drop vacuous decls;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Nov 21 21:38:08 2011 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Nov 21 23:03:31 2011 +0100
     1.3 @@ -281,6 +281,7 @@
     1.4          val facts' =
     1.5            if eq_list (eq_fst strict_eq_thm) (decls', fact') then
     1.6              [((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')]
     1.7 +          else if forall (null o snd) decls' then [((b, []), fact')]
     1.8            else [(empty_binding, decls'), ((b, []), fact')];
     1.9        in (facts', context') end)
    1.10    |> fst |> flat |> map (apsnd (map (apfst single)));