src/Pure/Isar/attrib.ML
changeset 45619 76c5f277b234
parent 45612 a3ed5b65b85e
child 46126 bab00660539d
     1.1 --- a/src/Pure/Isar/attrib.ML	Wed Nov 23 13:46:46 2011 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Nov 23 22:07:55 2011 +0100
     1.3 @@ -281,7 +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 if null decls' then [((b, []), fact')]
     1.9            else [(empty_binding, decls'), ((b, []), fact')];
    1.10        in (facts', context') end)
    1.11    |> fst |> flat |> map (apsnd (map (apfst single)));