--- a/src/HOL/Tools/rewrite_hol_proof.ML Mon Nov 16 21:56:32 2009 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Mon Nov 16 21:57:16 2009 +0100
@@ -7,7 +7,7 @@
signature REWRITE_HOL_PROOF =
sig
val rews: (Proofterm.proof * Proofterm.proof) list
- val elim_cong: typ list -> Proofterm.proof -> Proofterm.proof option
+ val elim_cong: typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
end;
structure RewriteHOLProof : REWRITE_HOL_PROOF =
@@ -309,17 +309,19 @@
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
-fun elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
+fun elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
- | elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
+ | elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
(strip_cong [] (incr_pboundvars 1 0 prf))
- | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
+ | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 [] o
apsnd (map (make_sym Ts))) (strip_cong [] prf1)
- | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
+ | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
- | elim_cong _ _ = NONE;
+ | elim_cong_aux _ _ = NONE;
+
+fun elim_cong Ts prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
end;