removing old code generator setup for inductive sets in the inductive set package
authorbulwahn
Wed, 19 Oct 2011 08:37:23 +0200
changeset 45177 189c81779a68
parent 45176 df4cbfc5ca4f
child 45178 fe9993491317
removing old code generator setup for inductive sets in the inductive set package
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]);