--- a/src/HOL/Extraction.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Extraction.thy Thu Jan 19 21:22:08 2006 +0100
@@ -35,16 +35,16 @@
incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $
Bound 0 $ incr_boundvars 1 s));
in
- [Extraction.add_types
+ Extraction.add_types
[("bool", ([], NONE)),
- ("set", ([realizes_set_proc], SOME mk_realizes_set))],
- Extraction.set_preprocessor (fn thy =>
+ ("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
Proofterm.rewrite_proof thy
(RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
- ProofRewriteRules.elim_vars (curry Const "arbitrary"))]
+ ProofRewriteRules.elim_vars (curry Const "arbitrary"))
end
*}