diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Extraction.thy
--- 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
 *}