cleanup code default attribute

--- a/src/HOL/Tools/datatype_package.ML	Tue Oct 28 12:29:57 2008 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Tue Oct 28 16:58:59 2008 +0100
@@ -200,7 +200,7 @@
   PureThy.add_thmss [(("simps", simps), []),
     (("", flat case_thms @
           flat distinct @ rec_thms), [Simplifier.simp_add]),
-    (("", rec_thms), [RecfunCodegen.add_default]),
+    (("", rec_thms), [Code.add_default_eqn_attribute]),
     (("", flat inject), [iff_add]),
     (("", map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
     (("", weak_case_congs), [cong_att])]

--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Oct 28 12:29:57 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Oct 28 16:58:59 2008 +0100
@@ -125,7 +125,7 @@
       val tinduct = map remove_domain_condition pinducts
 
       val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
-      val allatts = if has_guards then [] else [Attrib.internal (K RecfunCodegen.add_default)]
+      val allatts = if has_guards then [] else [Code.add_default_eqn_attrib]
 
       val qualify = NameSpace.qualified defname;
     in

--- a/src/HOL/Tools/old_primrec_package.ML	Tue Oct 28 12:29:57 2008 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Tue Oct 28 16:58:59 2008 +0100
@@ -284,7 +284,7 @@
     val simps'' = maps snd simps';
   in
     thy''
-    |> note (("simps", [Simplifier.simp_add, RecfunCodegen.add_default]), simps'')
+    |> note (("simps", [Simplifier.simp_add, Code.add_default_eqn_attribute]), simps'')
     |> snd
     |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
     |> snd

--- a/src/HOL/Tools/primrec_package.ML	Tue Oct 28 12:29:57 2008 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Tue Oct 28 16:58:59 2008 +0100
@@ -252,7 +252,7 @@
       (space_implode "_" (map (Sign.base_name o #1) defs));
     val spec' = (map o apfst o apfst) qualify spec;
     val simp_atts = map (Attrib.internal o K)
-      [Simplifier.simp_add, RecfunCodegen.add_default];
+      [Simplifier.simp_add, Code.add_default_eqn_attribute];
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())

--- a/src/HOL/Tools/recdef_package.ML	Tue Oct 28 12:29:57 2008 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Tue Oct 28 16:58:59 2008 +0100
@@ -208,7 +208,7 @@
         tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
                congs wfs name R eqs;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
-    val simp_att = if null tcs then [Simplifier.simp_add, RecfunCodegen.add_default] else [];
+    val simp_att = if null tcs then [Simplifier.simp_add, Code.add_default_eqn_attribute] else [];
 
     val ((simps' :: rules', [induct']), thy) =
       thy

--- a/src/HOL/Tools/recfun_codegen.ML	Tue Oct 28 12:29:57 2008 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue Oct 28 16:58:59 2008 +0100
@@ -7,9 +7,6 @@
 
 signature RECFUN_CODEGEN =
 sig
-  val add: string option -> attribute
-  val add_default: attribute
-  val del: attribute
   val setup: theory -> theory
 end;
 
@@ -27,24 +24,15 @@
   fun merge _ = Symtab.merge (K true);
 );
 
-fun add_thm add NONE thm thy = add thm thy
-  | add_thm add (SOME module_name) thm thy =
+fun add_thm NONE thm thy = Code.add_eqn thm thy
+  | add_thm (SOME module_name) thm thy =
       case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm
        of SOME (thm', _) => let val c = Code_Unit.const_eqn thm'
             in thy
               |> ModuleData.map (Symtab.update (c, module_name))
-              |> add thm'
+              |> Code.add_eqn thm'
             end
-        | NONE => add thm thy;
-
-fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
-  (add_thm Code.add_eqn opt_module thm) I);
-
-val add_default = Thm.declaration_attribute (fn thm => Context.mapping
-  (add_thm Code.add_default_eqn NONE thm) I);
-
-val del = Thm.declaration_attribute (fn thm => Context.mapping
-  (Code.del_eqn thm) I);
+        | NONE => Code.add_eqn thm thy;
 
 fun meta_eq_to_obj_eq thy thm =
   let
@@ -186,9 +174,15 @@
         end)
   | _ => NONE);
 
-val setup =
+val setup = let
+  fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
+    (add_thm opt_module thm) I);
+  val del = Thm.declaration_attribute (fn thm => Context.mapping
+    (Code.del_eqn thm) I);
+in
   add_codegen "recfun" recfun_codegen
   #> Code.add_attribute ("", Args.del |-- Scan.succeed del
-     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add);
+     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)
+end;
 
 end;

--- a/src/Pure/Isar/code.ML	Tue Oct 28 12:29:57 2008 +0100
+++ b/src/Pure/Isar/code.ML	Tue Oct 28 16:58:59 2008 +0100
@@ -11,7 +11,8 @@
   val add_eqn: thm -> theory -> theory
   val add_nonlinear_eqn: thm -> theory -> theory
   val add_default_eqn: thm -> theory -> theory
-  val add_default_eqn_attr: Attrib.src
+  val add_default_eqn_attribute: attribute
+  val add_default_eqn_attrib: Attrib.src
   val del_eqn: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
   val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory
@@ -571,8 +572,9 @@
       (fn thy => map (Code_Unit.assert_linear) o certify_const thy c) lthms;
   in change_eqns false c (add_lthms lthms') thy end;
 
-val add_default_eqn_attr = Attrib.internal (fn _ => Thm.declaration_attribute
-  (fn thm => Context.mapping (add_default_eqn thm) I));
+val add_default_eqn_attribute = Thm.declaration_attribute
+  (fn thm => Context.mapping (add_default_eqn thm) I);
+val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
 
 fun del_eqn thm thy = case mk_syntactic_eqn thy thm
  of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thm) (del_thm thm) thy
@@ -590,13 +592,9 @@
   let
     val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
     val (tyco, vs_cos) = Code_Unit.constrset_of_consts thy cs;
-    val cs' = map fst (snd vs_cos);
-    val purge_cs = case get_datatype thy tyco
-     of (_, []) => NONE
-      | (_, cos) => SOME (cs' @ map fst cos);
   in
     thy
-    |> map_exec_purge purge_cs
+    |> map_exec_purge NONE
         ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
         #> map_eqns (fold (Symtab.delete_safe o fst) cs))
     |> TypeInterpretation.data (tyco, serial ())

--- a/src/Pure/Isar/specification.ML	Tue Oct 28 12:29:57 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Oct 28 16:58:59 2008 +0100
@@ -184,7 +184,7 @@
     val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
         (var, ((Name.map_name (suffix "_raw") name, []), rhs));
     val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
-        ((name, Code.add_default_eqn_attr :: atts), [prove lthy2 th]);
+        ((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
 
     val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
     val _ =