# HG changeset patch
# User berghofe
# Date 1234783806 -3600
# Node ID 80a9a55b0a0e5afc83315ce8d270bee7feda91ac
# Parent  9e903a645d8f0c2490decb5f636f1253a2f86a65
Adapted to encoding of sets as predicates.

diff -r 9e903a645d8f -r 80a9a55b0a0e src/HOL/Extraction.thy
--- 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