src/HOL/Tools/rewrite_hol_proof.ML
changeset 15531 08c8dad8e399
parent 15530 6f43714517ee
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -286,10 +286,10 @@
     1.4  
     1.5  (** Replace congruence rules by substitution rules **)
     1.6  
     1.7 -fun strip_cong ps (PThm (("HOL.cong", _), _, _, _) % _ % _ % Some x % Some y %%
     1.8 +fun strip_cong ps (PThm (("HOL.cong", _), _, _, _) % _ % _ % SOME x % SOME y %%
     1.9        prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
    1.10 -  | strip_cong ps (PThm (("HOL.refl", _), _, _, _) % Some f) = Some (f, ps)
    1.11 -  | strip_cong _ _ = None;
    1.12 +  | strip_cong ps (PThm (("HOL.refl", _), _, _, _) % SOME f) = SOME (f, ps)
    1.13 +  | strip_cong _ _ = NONE;
    1.14  
    1.15  val subst_prf = fst (strip_combt (#2 (#der (rep_thm subst))));
    1.16  val sym_prf = fst (strip_combt (#2 (#der (rep_thm sym))));
    1.17 @@ -298,7 +298,7 @@
    1.18    | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
    1.19        let val T = fastype_of1 (Ts, x)
    1.20        in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
    1.21 -        else change_type (Some [T]) subst_prf %> x %> y %>
    1.22 +        else change_type (SOME [T]) subst_prf %> x %> y %>
    1.23            Abs ("z", T, list_comb (incr_boundvars 1 f,
    1.24              map (incr_boundvars 1) xs @ Bound 0 ::
    1.25              map (incr_boundvars 1 o snd o fst) ps)) %% prf' %%
    1.26 @@ -306,7 +306,7 @@
    1.27        end;
    1.28  
    1.29  fun make_sym Ts ((x, y), prf) =
    1.30 -  ((y, x), change_type (Some [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
    1.31 +  ((y, x), change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
    1.32  
    1.33  fun mk_AbsP P t = AbsP ("H", P, t);
    1.34  
    1.35 @@ -321,6 +321,6 @@
    1.36    | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % P %% prf) =
    1.37        apsome (mk_AbsP P o make_subst Ts (PBound 0) [] o
    1.38          apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
    1.39 -  | elim_cong _ _ = None;
    1.40 +  | elim_cong _ _ = NONE;
    1.41  
    1.42  end;