# HG changeset patch
# User wenzelm
# Date 1433159555 -7200
# Node ID a40b43121c5f17b3029aa1248384908bb5dfc9ff
# Parent  e85ed7a36b2ffec4811659356ee574474fdc7f9a
obsolete (see 189c81779a68);

diff -r e85ed7a36b2f -r a40b43121c5f src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Mon Jun 01 13:46:23 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Mon Jun 01 13:52:35 2015 +0200
@@ -24,7 +24,6 @@
     local_theory -> Inductive.inductive_result * local_theory
   val mono_add: attribute
   val mono_del: attribute
-  val codegen_preproc: theory -> thm list -> thm list
 end;
 
 structure Inductive_Set: INDUCTIVE_SET =
@@ -384,28 +383,6 @@
 val to_set_att = Thm.rule_attribute o to_set;
 
 
-(**** preprocessor for code generator ****)
-
-(* FIXME unused!? *)
-fun codegen_preproc thy =  (* FIXME proper context!? *)
-  let
-    val ctxt = Proof_Context.init_global thy;
-    val {to_pred_simps, set_arities, pred_arities, ...} =
-      Data.get (Context.Theory thy);
-    fun preproc thm =
-      if exists_Const (fn (s, _) => case Symtab.lookup set_arities s of
-          NONE => false
-        | SOME arities => exists (fn (_, (xs, _)) =>
-            forall is_none xs) arities) (Thm.prop_of thm)
-      then
-        thm |>
-        Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
-          [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
-        eta_contract_thm ctxt (is_pred pred_arities)
-      else thm
-  in map preproc end;
-
-
 (**** definition of inductive sets ****)
 
 fun add_ind_set_def