src/Pure/axclass.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15596 8665d08085df
     1.1 --- a/src/Pure/axclass.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  val is_def = Logic.is_equals o #prop o rep_thm;
     1.5  
     1.6  fun witnesses thy names thms =
     1.7 -  PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ filter is_def (map snd (axioms_of thy));
     1.8 +  PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ List.filter is_def (map snd (axioms_of thy));
     1.9  
    1.10  
    1.11  
    1.12 @@ -248,7 +248,7 @@
    1.13          [] => []
    1.14        | [(_, S)] => if Sign.subsort class_sign ([class], S) then S else err_bad_axsort name class
    1.15        | _ => err_bad_tfrees name);
    1.16 -    val axS = Sign.certify_sort class_sign (flat (map axm_sort axms));
    1.17 +    val axS = Sign.certify_sort class_sign (List.concat (map axm_sort axms));
    1.18  
    1.19      val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
    1.20      fun inclass c = Logic.mk_inclass (aT axS, c);
    1.21 @@ -288,7 +288,7 @@
    1.22  fun class_axms sign =
    1.23    let val classes = Sign.classes sign in
    1.24      map (Thm.class_triv sign) classes @
    1.25 -    mapfilter (apsome #intro o lookup_axclass_info_sg sign) classes
    1.26 +    List.mapPartial (Option.map #intro o lookup_axclass_info_sg sign) classes
    1.27    end;
    1.28  
    1.29  
    1.30 @@ -326,7 +326,7 @@
    1.31  
    1.32  fun axclass_tac thms =
    1.33    let
    1.34 -    val defs = filter is_def thms;
    1.35 +    val defs = List.filter is_def thms;
    1.36      val non_defs = filter_out is_def thms;
    1.37    in
    1.38      intro_classes_tac [] THEN
    1.39 @@ -338,7 +338,7 @@
    1.40  (* old-style provers *)
    1.41  
    1.42  fun prove mk_prop str_of sign prop thms usr_tac =
    1.43 -  (Tactic.prove sign [] [] (mk_prop prop) (K (axclass_tac thms THEN (if_none usr_tac all_tac)))
    1.44 +  (Tactic.prove sign [] [] (mk_prop prop) (K (axclass_tac thms THEN (getOpt (usr_tac,all_tac))))
    1.45      handle ERROR => error ("The error(s) above occurred while trying to prove " ^
    1.46       quote (str_of sign prop))) |> Drule.standard;
    1.47