src/HOL/Extraction.thy
changeset 18708 4b3dadb4fe33
parent 18511 beed2bc052a3
child 20941 beedcae49096
     1.1 --- a/src/HOL/Extraction.thy	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Extraction.thy	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -35,16 +35,16 @@
     1.4      incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $
     1.5        Bound 0 $ incr_boundvars 1 s));
     1.6  in
     1.7 -  [Extraction.add_types
     1.8 +  Extraction.add_types
     1.9        [("bool", ([], NONE)),
    1.10 -       ("set", ([realizes_set_proc], SOME mk_realizes_set))],
    1.11 -    Extraction.set_preprocessor (fn thy =>
    1.12 +       ("set", ([realizes_set_proc], SOME mk_realizes_set))] #>
    1.13 +  Extraction.set_preprocessor (fn thy =>
    1.14        Proofterm.rewrite_proof_notypes
    1.15          ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
    1.16            ProofRewriteRules.rprocs true) o
    1.17        Proofterm.rewrite_proof thy
    1.18          (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
    1.19 -      ProofRewriteRules.elim_vars (curry Const "arbitrary"))]
    1.20 +      ProofRewriteRules.elim_vars (curry Const "arbitrary"))
    1.21  end
    1.22  *}
    1.23