--- a/src/Pure/Proof/proof_rewrite_rules.ML Mon Nov 16 21:56:32 2009 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Mon Nov 16 21:57:16 2009 +0100
@@ -6,8 +6,9 @@
signature PROOF_REWRITE_RULES =
sig
- val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
- val rprocs : bool -> (typ list -> Proofterm.proof -> Proofterm.proof option) list
+ val rew : bool -> typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
+ val rprocs : bool ->
+ (typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
@@ -183,7 +184,7 @@
end
| rew' _ = NONE;
- in rew' end;
+ in rew' #> Option.map (rpair no_skel) end;
fun rprocs b = [rew b];
val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));