src/Pure/Isar/attrib.ML
changeset 46906 3c1787d46935
parent 46903 3d44892ac0d6
child 47005 421760a1efe7
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Mar 13 16:56:56 2012 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Mar 13 17:04:00 2012 +0100
     1.3 @@ -283,7 +283,8 @@
     1.4            else if null decls' then [((b, []), fact')]
     1.5            else [(empty_binding, decls'), ((b, []), fact')];
     1.6        in (facts', context') end)
     1.7 -  |> fst |> flat |> map (apsnd (map (apfst single)));
     1.8 +  |> fst |> flat |> map (apsnd (map (apfst single)))
     1.9 +  |> filter_out (fn (b, fact) => is_empty_binding b andalso forall (null o #2) fact);
    1.10  
    1.11  end;
    1.12