# HG changeset patch
# User berghofe
# Date 1033395032 -7200
# Node ID cfdf7e4cd0d20bd1a00edf533e5f29b613d9d9e0
# Parent  8bc77b17f59ffca0f5253ecb64478154d0b40794
Added elim_vars to preprocessor.

diff -r 8bc77b17f59f -r cfdf7e4cd0d2 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Mon Sep 30 16:09:05 2002 +0200
+++ b/src/HOL/Extraction.thy	Mon Sep 30 16:10:32 2002 +0200
@@ -19,7 +19,8 @@
         ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
           ProofRewriteRules.rprocs true) o
       Proofterm.rewrite_proof (Sign.tsig_of sg)
-        (RewriteHOLProof.rews, ProofRewriteRules.rprocs true)))
+        (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
+      ProofRewriteRules.elim_vars (curry Const "arbitrary")))
 *}
 
 lemmas [extraction_expand] =