--- a/src/HOL/Extraction.thy Mon Feb 16 20:45:15 2009 +1100
+++ b/src/HOL/Extraction.thy Mon Feb 16 12:30:06 2009 +0100
@@ -16,28 +16,19 @@
let
fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $
(Const ("op :", _) $ x $ S)) = (case strip_comb S of
- (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, binder_types U @
- [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x]))
- | (Free (s, U), ts) => SOME (list_comb (Free (s, binder_types U @
- [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x]))
+ (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, U), ts @ [x]))
+ | (Free (s, U), ts) => SOME (list_comb (Free (s, U), ts @ [x]))
| _ => NONE)
| realizes_set_proc (Const ("realizes", Type ("fun", [T, _])) $ r $
(Const ("op :", _) $ x $ S)) = (case strip_comb S of
- (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T :: binder_types U @
- [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), r :: ts @ [x]))
- | (Free (s, U), ts) => SOME (list_comb (Free (s, T :: binder_types U @
- [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), r :: ts @ [x]))
+ (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T --> U), r :: ts @ [x]))
+ | (Free (s, U), ts) => SOME (list_comb (Free (s, T --> U), r :: ts @ [x]))
| _ => NONE)
| realizes_set_proc _ = NONE;
-fun mk_realizes_set r rT s (setT as Type ("set", [elT])) =
- Abs ("x", elT, Const ("realizes", rT --> HOLogic.boolT --> HOLogic.boolT) $
- incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $
- Bound 0 $ incr_boundvars 1 s));
in
Extraction.add_types
- [("bool", ([], NONE)),
- ("set", ([realizes_set_proc], SOME mk_realizes_set))] #>
+ [("bool", ([], NONE))] #>
Extraction.set_preprocessor (fn thy =>
Proofterm.rewrite_proof_notypes
([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o