# HG changeset patch
# User bulwahn
# Date 1269243013 -3600
# Node ID 14a0993fe64b89901575e155400a23cb8ccad244
# Parent  c1f86c5d3827a4cc76d16b5f5ca8614036c7aeab
removed unused Predicate_Compile_Set

diff -r c1f86c5d3827 -r 14a0993fe64b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/IsaMakefile	Mon Mar 22 08:30:13 2010 +0100
@@ -301,7 +301,6 @@
   Tools/Predicate_Compile/predicate_compile_fun.ML \
   Tools/Predicate_Compile/predicate_compile.ML \
   Tools/Predicate_Compile/predicate_compile_pred.ML \
-  Tools/Predicate_Compile/predicate_compile_set.ML \
   Tools/quickcheck_generators.ML \
   Tools/Qelim/cooper_data.ML \
   Tools/Qelim/cooper.ML \
diff -r c1f86c5d3827 -r 14a0993fe64b src/HOL/Predicate_Compile.thy
--- a/src/HOL/Predicate_Compile.thy	Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Predicate_Compile.thy	Mon Mar 22 08:30:13 2010 +0100
@@ -10,7 +10,6 @@
 uses
   "Tools/Predicate_Compile/predicate_compile_aux.ML"
   "Tools/Predicate_Compile/predicate_compile_core.ML"
-  "Tools/Predicate_Compile/predicate_compile_set.ML"
   "Tools/Predicate_Compile/predicate_compile_data.ML"
   "Tools/Predicate_Compile/predicate_compile_fun.ML"
   "Tools/Predicate_Compile/predicate_compile_pred.ML"
diff -r c1f86c5d3827 -r 14a0993fe64b src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML	Mon Mar 22 08:30:13 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_set.ML
-    Author:     Lukas Bulwahn, TU Muenchen
-
-Preprocessing sets to predicates.
-*)
-
-signature PREDICATE_COMPILE_SET =
-sig
-(*
-  val preprocess_intro : thm -> theory -> thm * theory
-  val preprocess_clause : term -> theory -> term * theory
-*)
-  val unfold_set_notation : thm -> thm;
-end;
-
-structure Predicate_Compile_Set : PREDICATE_COMPILE_SET =
-struct
-(*FIXME: unfolding Ball in pretty adhoc here *)
-val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def},
-@{thm Ball_def}, @{thm Bex_def}]
-
-val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
-
-(*
-fun find_set_theorems ctxt cname =
-  let
-    val _ = cname 
-*)
-
-(*
-fun preprocess_term t ctxt =
-  case t of
-    Const ("op :", _) $ x $ A => 
-      case strip_comb A of
-        (Const (cname, T), params) =>
-          let 
-            val _ = find_set_theorems
-          in
-            (t, ctxt)
-          end
-      | _ => (t, ctxt)  
-  | _ => (t, ctxt)
-*) 
-(*
-fun preprocess_intro th thy =
-  let
-    val cnames = find_heads_of_prems
-    val set_cname = filter (has_set_definition
-    val _ = define_preds
-    val _ = prep_pred_def
-  in
-*)
-end;