# HG changeset patch
# User bulwahn
# Date 1319006243 -7200
# Node ID 189c81779a683a5f96693d9911bd8cad40a428a5
# Parent  df4cbfc5ca4f9d5fa6988a79664dff6beee8c0e2
removing old code generator setup for inductive sets in the inductive set package

diff -r df4cbfc5ca4f -r 189c81779a68 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Oct 19 08:37:22 2011 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Wed Oct 19 08:37:23 2011 +0200
@@ -401,7 +401,7 @@
       else thm
   in map preproc end;
 
-fun code_ind_att optmod = to_pred_att [] #> Inductive_Codegen.add optmod NONE;
+fun code_ind_att optmod = to_pred_att [];
 
 
 (**** definition of inductive sets ****)
@@ -551,10 +551,6 @@
     "convert rule to set notation" #>
   Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att)
     "convert rule to predicate notation" #>
-  Attrib.setup @{binding code_ind_set}
-    (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att))
-    "introduction rules for executable predicates" #>
-  Codegen.add_preprocessor codegen_preproc #>
   Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
     "declaration of monotonicity rule for set operators" #>
   Simplifier.map_simpset_global (fn ss => ss addsimprocs [collect_mem_simproc]);