src/HOL/Tools/datatype_realizer.ML
changeset 15531 08c8dad8e399
parent 15256 9237f388fbb1
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4  
     1.5  fun forall_intr_prf (t, prf) =
     1.6    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
     1.7 -  in Abst (a, Some T, Proofterm.prf_abstract_over t prf) end;
     1.8 +  in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
     1.9  
    1.10  fun prf_of thm =
    1.11    let val {sign, prop, der = (_, prf), ...} = rep_thm thm
    1.12 @@ -108,9 +108,9 @@
    1.13          (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
    1.14      val r = if null is then Extraction.nullt else
    1.15        foldr1 HOLogic.mk_prod (mapfilter (fn (((((i, _), T), U), s), tname) =>
    1.16 -        if i mem is then Some
    1.17 +        if i mem is then SOME
    1.18            (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
    1.19 -        else None) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
    1.20 +        else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
    1.21      val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
    1.22        (map (fn ((((i, _), T), U), tname) =>
    1.23          make_pred i U T (mk_proj i is r) (Free (tname, T)))
    1.24 @@ -149,10 +149,10 @@
    1.25          (case head_of (strip_abs_body f) of
    1.26             Free (s, T) =>
    1.27               let val T' = Type.varifyT T
    1.28 -             in Abst (s, Some T', Proofterm.prf_abstract_over
    1.29 -               (Var ((s, 0), T')) (AbsP ("H", Some p, prf)))
    1.30 +             in Abst (s, SOME T', Proofterm.prf_abstract_over
    1.31 +               (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
    1.32               end
    1.33 -         | _ => AbsP ("H", Some p, prf)))
    1.34 +         | _ => AbsP ("H", SOME p, prf)))
    1.35             (rec_fns ~~ prems_of thm, Proofterm.proof_combP
    1.36               (prf_of thm', map PBound (length prems - 1 downto 0))));
    1.37  
    1.38 @@ -183,7 +183,7 @@
    1.39              list_comb (r, free_ts)))))
    1.40        end;
    1.41  
    1.42 -    val Some (_, _, constrs) = assoc (descr, index);
    1.43 +    val SOME (_, _, constrs) = assoc (descr, index);
    1.44      val T = nth_elem (index, get_rec_types descr sorts);
    1.45      val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
    1.46      val r = Const (case_name, map fastype_of rs ---> T --> rT);
    1.47 @@ -210,7 +210,7 @@
    1.48      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    1.49      val prf = forall_intr_prf (y, forall_intr_prf (P,
    1.50        foldr (fn ((p, r), prf) =>
    1.51 -        forall_intr_prf (Logic.varify r, AbsP ("H", Some (Logic.varify p),
    1.52 +        forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
    1.53            prf))) (prems ~~ rs, Proofterm.proof_combP (prf_of thm',
    1.54              map PBound (length prems - 1 downto 0)))));
    1.55      val r' = Logic.varify (Abs ("y", Type.varifyT T,