src/HOL/Extraction.thy
changeset 33723 14d0dadd9517
parent 33704 6aeb8454efc1
child 34913 d8cb720c9c53
     1.1 --- a/src/HOL/Extraction.thy	Mon Nov 16 21:57:16 2009 +0100
     1.2 +++ b/src/HOL/Extraction.thy	Tue Nov 17 14:48:21 2009 +0100
     1.3 @@ -13,20 +13,6 @@
     1.4  subsection {* Setup *}
     1.5  
     1.6  setup {*
     1.7 -let
     1.8 -fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $
     1.9 -      (Const ("op :", _) $ x $ S)) = (case strip_comb S of
    1.10 -        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, U), ts @ [x]))
    1.11 -      | (Free (s, U), ts) => SOME (list_comb (Free (s, U), ts @ [x]))
    1.12 -      | _ => NONE)
    1.13 -  | realizes_set_proc (Const ("realizes", Type ("fun", [T, _])) $ r $
    1.14 -      (Const ("op :", _) $ x $ S)) = (case strip_comb S of
    1.15 -        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T --> U), r :: ts @ [x]))
    1.16 -      | (Free (s, U), ts) => SOME (list_comb (Free (s, T --> U), r :: ts @ [x]))
    1.17 -      | _ => NONE)
    1.18 -  | realizes_set_proc _ = NONE;
    1.19 -
    1.20 -in
    1.21    Extraction.add_types
    1.22        [("bool", ([], NONE))] #>
    1.23    Extraction.set_preprocessor (fn thy =>
    1.24 @@ -35,7 +21,6 @@
    1.25        Proofterm.rewrite_proof thy
    1.26          (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
    1.27        ProofRewriteRules.elim_vars (curry Const @{const_name default}))
    1.28 -end
    1.29  *}
    1.30  
    1.31  lemmas [extraction_expand] =