src/HOL/Tools/datatype_aux.ML
changeset 15531 08c8dad8e399
parent 15379 830239e6eb73
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -130,11 +130,11 @@
     1.4      val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
     1.5        (Logic.strip_imp_concl (nth_elem (i - 1, prems_of st))));
     1.6      val getP = if can HOLogic.dest_imp (hd ts) then
     1.7 -      (apfst Some) o HOLogic.dest_imp else pair None;
     1.8 +      (apfst SOME) o HOLogic.dest_imp else pair NONE;
     1.9      fun abstr (t1, t2) = (case t1 of
    1.10 -        None => let val [Free (s, T)] = add_term_frees (t2, [])
    1.11 +        NONE => let val [Free (s, T)] = add_term_frees (t2, [])
    1.12            in absfree (s, T, t2) end
    1.13 -      | Some (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
    1.14 +      | SOME (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
    1.15      val cert = cterm_of (Thm.sign_of_thm st);
    1.16      val Ps = map (cert o head_of o snd o getP) ts;
    1.17      val indrule' = cterm_instantiate (Ps ~~
    1.18 @@ -197,8 +197,8 @@
    1.19  
    1.20  fun subst_DtTFree _ substs (T as (DtTFree name)) =
    1.21        (case assoc (substs, name) of
    1.22 -         None => T
    1.23 -       | Some U => U)
    1.24 +         NONE => T
    1.25 +       | SOME U => U)
    1.26    | subst_DtTFree i substs (DtType (name, ts)) =
    1.27        DtType (name, map (subst_DtTFree i substs) ts)
    1.28    | subst_DtTFree i _ (DtRec j) = DtRec (i + j);
    1.29 @@ -237,8 +237,8 @@
    1.30    | dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
    1.31    | dtyp_of_typ new_dts (Type (tname, Ts)) =
    1.32        (case assoc (new_dts, tname) of
    1.33 -         None => DtType (tname, map (dtyp_of_typ new_dts) Ts)
    1.34 -       | Some vs => if map (try dest_TFree) Ts = map Some vs then
    1.35 +         NONE => DtType (tname, map (dtyp_of_typ new_dts) Ts)
    1.36 +       | SOME vs => if map (try dest_TFree) Ts = map SOME vs then
    1.37               DtRec (find_index (curry op = tname o fst) new_dts)
    1.38             else error ("Illegal occurence of recursive type " ^ tname));
    1.39  
    1.40 @@ -300,9 +300,9 @@
    1.41  
    1.42      fun get_dt_descr T i tname dts =
    1.43        (case Symtab.lookup (dt_info, tname) of
    1.44 -         None => typ_error T (tname ^ " is not a datatype - can't use it in\
    1.45 +         NONE => typ_error T (tname ^ " is not a datatype - can't use it in\
    1.46             \ nested recursion")
    1.47 -       | (Some {index, descr, ...}) =>
    1.48 +       | (SOME {index, descr, ...}) =>
    1.49             let val (_, vars, _) = the (assoc (descr, index));
    1.50                 val subst = ((map dest_DtTFree vars) ~~ dts) handle LIST _ =>
    1.51                   typ_error T ("Type constructor " ^ tname ^ " used with wrong\