src/Pure/context.ML

      (check_thy thy1; check_thy thy2;
       create_thy draftN NONE (serial (), draftN) ids iids data ancestry history))
   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)
   else
     let