src/HOL/Tools/rewrite_hol_proof.ML
changeset 33722 e588744f14da
parent 33388 d64545e6cba5
child 35845 e5980f0ad025
--- 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;