Added setup.
--- a/src/Pure/Proof/proof_rewrite_rules.ML Mon Nov 19 17:39:31 2001 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Mon Nov 19 17:40:07 2001 +0100
@@ -10,6 +10,7 @@
signature PROOF_REWRITE_RULES =
sig
val rprocs : (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
+ val setup : (theory -> theory) list
end;
structure ProofRewriteRules : PROOF_REWRITE_RULES =
@@ -111,7 +112,6 @@
| rew _ _ = None;
val rprocs = [("Pure/meta_equality", rew)];
+val setup = [Proofterm.add_prf_rprocs rprocs];
end;
-
-Proofterm.add_prf_rprocs ProtoPure.thy ProofRewriteRules.rprocs;