# HG changeset patch
# User wenzelm
# Date 1258465701 -3600
# Node ID 14d0dadd9517a5ec82496aa1a7aaa512a206a8c3
# Parent  e588744f14dabc1bb5944513cc344df7949e7840
eliminated dead code;

diff -r e588744f14da -r 14d0dadd9517 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Mon Nov 16 21:57:16 2009 +0100
+++ b/src/HOL/Extraction.thy	Tue Nov 17 14:48:21 2009 +0100
@@ -13,20 +13,6 @@
 subsection {* Setup *}
 
 setup {*
-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, 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 --> U), r :: ts @ [x]))
-      | (Free (s, U), ts) => SOME (list_comb (Free (s, T --> U), r :: ts @ [x]))
-      | _ => NONE)
-  | realizes_set_proc _ = NONE;
-
-in
   Extraction.add_types
       [("bool", ([], NONE))] #>
   Extraction.set_preprocessor (fn thy =>
@@ -35,7 +21,6 @@
       Proofterm.rewrite_proof thy
         (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
       ProofRewriteRules.elim_vars (curry Const @{const_name default}))
-end
 *}
 
 lemmas [extraction_expand] =