src/Pure/axclass.ML

 (* get axioms and theorems *)
 
 val is_def = Logic.is_equals o #prop o rep_thm;
 
 fun witnesses thy names thms =
-  PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ filter is_def (map snd (axioms_of thy));
+  PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ List.filter is_def (map snd (axioms_of thy));
 
 
 
 (** abstract syntax operations **)
 

     fun axm_sort (name, ax) =
       (case term_tfrees ax of
         [] => []
       | [(_, S)] => if Sign.subsort class_sign ([class], S) then S else err_bad_axsort name class
       | _ => err_bad_tfrees name);
-    val axS = Sign.certify_sort class_sign (flat (map axm_sort axms));
+    val axS = Sign.certify_sort class_sign (List.concat (map axm_sort axms));
 
     val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
     fun inclass c = Logic.mk_inclass (aT axS, c);
 
     val intro_axm = Logic.list_implies

 (* class_axms *)
 
 fun class_axms sign =
   let val classes = Sign.classes sign in
     map (Thm.class_triv sign) classes @
-    mapfilter (apsome #intro o lookup_axclass_info_sg sign) classes
+    List.mapPartial (Option.map #intro o lookup_axclass_info_sg sign) classes
   end;
 
 
 (* intro_classes *)
 

   (2) rewrite goals using user supplied definitions
   (3) repeatedly resolve goals with user supplied non-definitions*)
 
 fun axclass_tac thms =
   let
-    val defs = filter is_def thms;
+    val defs = List.filter is_def thms;
     val non_defs = filter_out is_def thms;
   in
     intro_classes_tac [] THEN
     TRY (rewrite_goals_tac defs) THEN
     TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))

 
 
 (* old-style provers *)
 
 fun prove mk_prop str_of sign prop thms usr_tac =
-  (Tactic.prove sign [] [] (mk_prop prop) (K (axclass_tac thms THEN (if_none usr_tac all_tac)))
+  (Tactic.prove sign [] [] (mk_prop prop) (K (axclass_tac thms THEN (getOpt (usr_tac,all_tac))))
     handle ERROR => error ("The error(s) above occurred while trying to prove " ^
      quote (str_of sign prop))) |> Drule.standard;
 
 val prove_subclass = prove mk_classrel (fn sg => fn (c1, c2) =>
   Pretty.string_of_classrel (Sign.pp sg) [c1, c2]);