src/HOL/Extraction.thy
changeset 29930 80a9a55b0a0e
parent 28797 9dcd32ee5dbe
child 30235 58d147683393
     1.1 --- a/src/HOL/Extraction.thy	Mon Feb 16 20:45:15 2009 +1100
     1.2 +++ b/src/HOL/Extraction.thy	Mon Feb 16 12:30:06 2009 +0100
     1.3 @@ -16,28 +16,19 @@
     1.4  let
     1.5  fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $
     1.6        (Const ("op :", _) $ x $ S)) = (case strip_comb S of
     1.7 -        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, binder_types U @
     1.8 -           [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x]))
     1.9 -      | (Free (s, U), ts) => SOME (list_comb (Free (s, binder_types U @
    1.10 -           [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x]))
    1.11 +        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, U), ts @ [x]))
    1.12 +      | (Free (s, U), ts) => SOME (list_comb (Free (s, U), ts @ [x]))
    1.13        | _ => NONE)
    1.14    | realizes_set_proc (Const ("realizes", Type ("fun", [T, _])) $ r $
    1.15        (Const ("op :", _) $ x $ S)) = (case strip_comb S of
    1.16 -        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T :: binder_types U @
    1.17 -           [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), r :: ts @ [x]))
    1.18 -      | (Free (s, U), ts) => SOME (list_comb (Free (s, T :: binder_types U @
    1.19 -           [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), r :: ts @ [x]))
    1.20 +        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T --> U), r :: ts @ [x]))
    1.21 +      | (Free (s, U), ts) => SOME (list_comb (Free (s, T --> U), r :: ts @ [x]))
    1.22        | _ => NONE)
    1.23    | realizes_set_proc _ = NONE;
    1.24  
    1.25 -fun mk_realizes_set r rT s (setT as Type ("set", [elT])) =
    1.26 -  Abs ("x", elT, Const ("realizes", rT --> HOLogic.boolT --> HOLogic.boolT) $
    1.27 -    incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $
    1.28 -      Bound 0 $ incr_boundvars 1 s));
    1.29  in
    1.30    Extraction.add_types
    1.31 -      [("bool", ([], NONE)),
    1.32 -       ("set", ([realizes_set_proc], SOME mk_realizes_set))] #>
    1.33 +      [("bool", ([], NONE))] #>
    1.34    Extraction.set_preprocessor (fn thy =>
    1.35        Proofterm.rewrite_proof_notypes
    1.36          ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o