src/HOL/Extraction.thy
changeset 16121 a80aa66d2271
parent 15531 08c8dad8e399
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Extraction.thy	Tue May 31 11:53:11 2005 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Tue May 31 11:53:12 2005 +0200
     1.3 @@ -12,7 +12,8 @@
     1.4  
     1.5  subsection {* Setup *}
     1.6  
     1.7 -ML_setup {*
     1.8 +setup {*
     1.9 +let
    1.10  fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $
    1.11        (Const ("op :", _) $ x $ S)) = (case strip_comb S of
    1.12          (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, binder_types U @
    1.13 @@ -33,18 +34,18 @@
    1.14    Abs ("x", elT, Const ("realizes", rT --> HOLogic.boolT --> HOLogic.boolT) $
    1.15      incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $
    1.16        Bound 0 $ incr_boundvars 1 s));
    1.17 -
    1.18 -  Context.>> (fn thy => thy |>
    1.19 -    Extraction.add_types
    1.20 +in
    1.21 +  [Extraction.add_types
    1.22        [("bool", ([], NONE)),
    1.23 -       ("set", ([realizes_set_proc], SOME mk_realizes_set))] |>
    1.24 +       ("set", ([realizes_set_proc], SOME mk_realizes_set))],
    1.25      Extraction.set_preprocessor (fn sg =>
    1.26        Proofterm.rewrite_proof_notypes
    1.27          ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
    1.28            ProofRewriteRules.rprocs true) o
    1.29        Proofterm.rewrite_proof (Sign.tsig_of sg)
    1.30          (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
    1.31 -      ProofRewriteRules.elim_vars (curry Const "arbitrary")))
    1.32 +      ProofRewriteRules.elim_vars (curry Const "arbitrary"))]
    1.33 +end
    1.34  *}
    1.35  
    1.36  lemmas [extraction_expand] =