Added setup.
authorberghofe
Mon, 19 Nov 2001 17:40:07 +0100
changeset 12237 39aeccee9e1c
parent 12236 67a617b231aa
child 12238 09966ccbc84c
Added setup.
src/Pure/Proof/proof_rewrite_rules.ML
--- 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;