# HG changeset patch
# User berghofe
# Date 1006188007 -3600
# Node ID 39aeccee9e1c32e975404cb1c338dc254502ede4
# Parent  67a617b231aa539bdbd44992f06a35635d31c18c
Added setup.

diff -r 67a617b231aa -r 39aeccee9e1c 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;