src/HOL/Tools/rewrite_hol_proof.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 19798 94f12468bbba
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -311,15 +311,15 @@
     1.4  fun mk_AbsP P t = AbsP ("H", P, t);
     1.5  
     1.6  fun elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % _ % _ %% prf1 %% prf2) =
     1.7 -      apsome (make_subst Ts prf2 []) (strip_cong [] prf1)
     1.8 +      Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
     1.9    | elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % P % _ %% prf) =
    1.10 -      apsome (mk_AbsP P o make_subst Ts (PBound 0) [])
    1.11 +      Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
    1.12          (strip_cong [] (incr_pboundvars 1 0 prf))
    1.13    | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % _ %% prf1 %% prf2) =
    1.14 -      apsome (make_subst Ts prf2 [] o
    1.15 +      Option.map (make_subst Ts prf2 [] o
    1.16          apsnd (map (make_sym Ts))) (strip_cong [] prf1)
    1.17    | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % P %% prf) =
    1.18 -      apsome (mk_AbsP P o make_subst Ts (PBound 0) [] o
    1.19 +      Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
    1.20          apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
    1.21    | elim_cong _ _ = NONE;
    1.22