--- a/src/Pure/Isar/attrib.ML Wed Nov 23 13:46:46 2011 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Nov 23 22:07:55 2011 +0100
@@ -281,7 +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 if null decls' then [((b, []), fact')]
else [(empty_binding, decls'), ((b, []), fact')];
in (facts', context') end)
|> fst |> flat |> map (apsnd (map (apfst single)));