src/HOL/Tools/typedef_package.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 16126 3ba9eb7ea366
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -104,9 +104,9 @@
     1.4      val thms = PureThy.get_thmss thy (map (rpair NONE) witn_names) @ witn_thms;
     1.5      val tac =
     1.6        witn1_tac THEN
     1.7 -      TRY (rewrite_goals_tac (filter is_def thms)) THEN
     1.8 +      TRY (rewrite_goals_tac (List.filter is_def thms)) THEN
     1.9        TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN
    1.10 -      if_none witn2_tac (TRY (ALLGOALS (CLASET' blast_tac)));
    1.11 +      getOpt (witn2_tac, TRY (ALLGOALS (CLASET' blast_tac)));
    1.12    in
    1.13      message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
    1.14      Tactic.prove (Theory.sign_of thy) [] [] goal (K tac)
    1.15 @@ -144,12 +144,12 @@
    1.16      val goal_pat = mk_nonempty (Var (vname, setT));
    1.17  
    1.18      (*lhs*)
    1.19 -    val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.typeS)) vs;
    1.20 +    val lhs_tfrees = map (fn v => (v, getOpt (assoc (rhs_tfrees, v), HOLogic.typeS))) vs;
    1.21      val tname = Syntax.type_name t mx;
    1.22      val full_tname = full tname;
    1.23      val newT = Type (full_tname, map TFree lhs_tfrees);
    1.24  
    1.25 -    val (Rep_name, Abs_name) = if_none opt_morphs ("Rep_" ^ name, "Abs_" ^ name);
    1.26 +    val (Rep_name, Abs_name) = getOpt (opt_morphs, ("Rep_" ^ name, "Abs_" ^ name));
    1.27      val setC = Const (full_name, setT);
    1.28      val RepC = Const (full Rep_name, newT --> oldT);
    1.29      val AbsC = Const (full Abs_name, oldT --> newT);
    1.30 @@ -251,7 +251,7 @@
    1.31  
    1.32  fun sane_typedef prep_term def opt_name typ set opt_morphs tac =
    1.33    gen_typedef prep_term def
    1.34 -    (if_none opt_name (#1 typ)) typ set opt_morphs all_tac [] [] (SOME tac);
    1.35 +    (getOpt (opt_name, #1 typ)) typ set opt_morphs all_tac [] [] (SOME tac);
    1.36  
    1.37  fun add_typedef_x name typ set names thms tac =
    1.38    #1 o gen_typedef read_term true name typ set NONE (Tactic.rtac exI 1) names thms tac;
    1.39 @@ -287,8 +287,8 @@
    1.40        in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
    1.41      fun get_name (Type (tname, _)) = tname
    1.42        | get_name _ = "";
    1.43 -    fun lookup f T = if_none (apsome f (Symtab.lookup
    1.44 -      (TypedefData.get thy, get_name T))) ""
    1.45 +    fun lookup f T = getOpt (Option.map f (Symtab.lookup
    1.46 +      (TypedefData.get thy, get_name T)), "")
    1.47    in
    1.48      (case strip_comb t of
    1.49         (Const (s, Type ("fun", [T, U])), ts) =>
    1.50 @@ -310,7 +310,7 @@
    1.51        (case Symtab.lookup (TypedefData.get thy, s) of
    1.52           NONE => NONE
    1.53         | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
    1.54 -           if is_some (Codegen.get_assoc_type thy tname) then NONE else
    1.55 +           if isSome (Codegen.get_assoc_type thy tname) then NONE else
    1.56             let
    1.57               val sg = sign_of thy;
    1.58               val Abs_id = Codegen.mk_const_id sg Abs_name;
    1.59 @@ -382,7 +382,7 @@
    1.60      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
    1.61  
    1.62  fun mk_typedef_proof ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
    1.63 -  typedef_proof ((def, if_none opt_name (Syntax.type_name t mx)), (t, vs, mx), A, morphs);
    1.64 +  typedef_proof ((def, getOpt (opt_name, Syntax.type_name t mx)), (t, vs, mx), A, morphs);
    1.65  
    1.66  val typedefP =
    1.67    OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal