# HG changeset patch
# User wenzelm
# Date 1226781073 -3600
# Node ID 9dcd32ee5dbe6fb4afb7b5c71600103b65f41723
# Parent  56cb4130177aa9cbc6cdf917bafd7bfbfceac79f
rewrite_proof: simplified simprocs (no name required);

diff -r 56cb4130177a -r 9dcd32ee5dbe src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Sat Nov 15 11:25:17 2008 +0100
+++ b/src/HOL/Extraction.thy	Sat Nov 15 21:31:13 2008 +0100
@@ -40,8 +40,7 @@
        ("set", ([realizes_set_proc], SOME mk_realizes_set))] #>
   Extraction.set_preprocessor (fn thy =>
       Proofterm.rewrite_proof_notypes
-        ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
-          ProofRewriteRules.rprocs true) o
+        ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
       Proofterm.rewrite_proof thy
         (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
       ProofRewriteRules.elim_vars (curry Const @{const_name default}))