src/HOL/Extraction.thy
changeset 28797 9dcd32ee5dbe
parent 27982 2aaa4a5569a6
child 29930 80a9a55b0a0e
     1.1 --- a/src/HOL/Extraction.thy	Sat Nov 15 11:25:17 2008 +0100
     1.2 +++ b/src/HOL/Extraction.thy	Sat Nov 15 21:31:13 2008 +0100
     1.3 @@ -40,8 +40,7 @@
     1.4         ("set", ([realizes_set_proc], SOME mk_realizes_set))] #>
     1.5    Extraction.set_preprocessor (fn thy =>
     1.6        Proofterm.rewrite_proof_notypes
     1.7 -        ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
     1.8 -          ProofRewriteRules.rprocs true) o
     1.9 +        ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
    1.10        Proofterm.rewrite_proof thy
    1.11          (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
    1.12        ProofRewriteRules.elim_vars (curry Const @{const_name default}))