Added elim_vars to preprocessor.
authorberghofe
Mon Sep 30 16:10:32 2002 +0200 (2002-09-30)
changeset 13599cfdf7e4cd0d2
parent 13598 8bc77b17f59f
child 13600 9702c8636a7b
Added elim_vars to preprocessor.
src/HOL/Extraction.thy
     1.1 --- a/src/HOL/Extraction.thy	Mon Sep 30 16:09:05 2002 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Mon Sep 30 16:10:32 2002 +0200
     1.3 @@ -19,7 +19,8 @@
     1.4          ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
     1.5            ProofRewriteRules.rprocs true) o
     1.6        Proofterm.rewrite_proof (Sign.tsig_of sg)
     1.7 -        (RewriteHOLProof.rews, ProofRewriteRules.rprocs true)))
     1.8 +        (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
     1.9 +      ProofRewriteRules.elim_vars (curry Const "arbitrary")))
    1.10  *}
    1.11  
    1.12  lemmas [extraction_expand] =