1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 16 21:56:32 2009 +0100
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 16 21:57:16 2009 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  signature REWRITE_HOL_PROOF =
     1.5  sig
     1.6    val rews: (Proofterm.proof * Proofterm.proof) list
     1.7 -  val elim_cong: typ list -> Proofterm.proof -> Proofterm.proof option
     1.8 +  val elim_cong: typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
     1.9  end;
    1.10  
    1.11  structure RewriteHOLProof : REWRITE_HOL_PROOF =
    1.12 @@ -309,17 +309,19 @@
    1.13  
    1.14  fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
    1.15  
    1.16 -fun elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
    1.17 +fun elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
    1.18        Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
    1.19 -  | elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
    1.20 +  | elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
    1.21        Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
    1.22          (strip_cong [] (incr_pboundvars 1 0 prf))
    1.23 -  | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
    1.24 +  | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
    1.25        Option.map (make_subst Ts prf2 [] o
    1.26          apsnd (map (make_sym Ts))) (strip_cong [] prf1)
    1.27 -  | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
    1.28 +  | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
    1.29        Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
    1.30          apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
    1.31 -  | elim_cong _ _ = NONE;
    1.32 +  | elim_cong_aux _ _ = NONE;
    1.33 +
    1.34 +fun elim_cong Ts prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
    1.35  
    1.36  end;