| changeset 28617 | c9c1c8b28a62 |
| parent 28375 | c879d88d038a |
| child 29001 | b97a3f808133 |
--- a/src/Pure/context.ML Thu Oct 16 22:44:25 2008 +0200 +++ b/src/Pure/context.ML Thu Oct 16 22:44:26 2008 +0200 @@ -356,7 +356,7 @@ in thy' end; fun maximal_thys thys = - thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys)); + thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys); fun begin_thy pp name imports = if name = draftN then error ("Illegal theory name: " ^ quote draftN)