src/HOL/Tools/datatype_codegen.ML

 
   type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
     -> theory -> theory
   val codetype_hook: hook
   val eq_hook: hook
-  val codetypes_dependency: theory -> (string * bool) list list
-  val add_codetypes_hook_bootstrap: hook -> theory -> theory
+  val add_codetypes_hook: hook -> theory -> theory
   val the_codetypes_mut_specs: theory -> (string * bool) list
     -> ((string * sort) list * (string * (bool * (string * typ list) list)) list)
   val get_codetypes_arities: theory -> (string * bool) list -> sort
-    -> (string * (arity * term list)) list option
+    -> (string * (arity * term list)) list
   val prove_codetypes_arities: tactic -> (string * bool) list -> sort
     -> (arity list -> (string * term list) list -> theory
       -> ((bstring * Attrib.src list) * term) list * theory)
     -> (arity list -> (string * term list) list -> thm list -> theory -> theory)
     -> theory -> theory

 
 (** codetypes for code 2nd generation **)
 
 (* abstraction over datatypes vs. type copies *)
 
+fun get_spec thy (dtco, true) =
+      (the o DatatypePackage.get_datatype_spec thy) dtco
+  | get_spec thy (tyco, false) =
+      TypecopyPackage.get_spec thy tyco;
+
 fun codetypes_dependency thy =
   let
     val names =
       map (rpair true) (Symtab.keys (DatatypePackage.get_datatypes thy))
         @ map (rpair false) (TypecopyPackage.get_typecopies thy);

     Graph.empty
     |> fold add_node names
     |> Graph.strong_conn
     |> map (AList.make (the o AList.lookup (op =) names))
   end;
-
-fun get_spec thy (dtco, true) =
-      (the o DatatypePackage.get_datatype_spec thy) dtco
-  | get_spec thy (tyco, false) =
-      TypecopyPackage.get_spec thy tyco;
 
 local
   fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    of SOME _ => get_eq_datatype thy tyco
     | NONE => [TypecopyPackage.get_eq thy tyco];

 end;
 
 type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
   -> theory -> theory;
 
-fun add_codetypes_hook_bootstrap hook thy =
+fun add_codetypes_hook hook thy =
   let
     fun add_spec thy (tyco, is_dt) =
       (tyco, (is_dt, get_spec thy (tyco, is_dt)));
     fun datatype_hook dtcos thy =
       hook (map (add_spec thy) (map (rpair true) dtcos)) thy;
     fun typecopy_hook ((tyco, _)) thy =
       hook ([(tyco, (false, TypecopyPackage.get_spec thy tyco))]) thy;
   in
     thy
     |> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy))
-    |> DatatypeHooks.add datatype_hook
-    |> TypecopyPackage.add_hook typecopy_hook
+    |> DatatypePackage.add_interpretator datatype_hook
+    |> TypecopyPackage.add_interpretator typecopy_hook
   end;
 
 fun the_codetypes_mut_specs thy ([(tyco, is_dt)]) =
       let
         val (vs, cs) = get_spec thy (tyco, is_dt)

         val tys' = (map o Term.map_type_tfree) (TFree o inst) tys;
         val ts = Name.names Name.context "a" tys';
         val ty = (tys' ---> Type (tyco, map TFree vs'));
       in list_comb (Const (c, ty), map Free ts) end;
   in
-    map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css |> SOME
-  end handle Class_Error => NONE;
+    map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
+  end;
 
 fun prove_codetypes_arities tac tycos sort f after_qed thy =
-  case get_codetypes_arities thy tycos sort
+  case try (get_codetypes_arities thy tycos) sort
    of NONE => thy
     | SOME insts => let
         fun proven (tyco, asorts, sort) =
           Sorts.of_sort (Sign.classes_of thy)
             (Type (tyco, map TFree (Name.names Name.context "'a" asorts)), sort);

     fold_rev Code.add_default_func case_rewrites thy
   end;
 
 val setup = 
   add_codegen "datatype" datatype_codegen
-  #> add_tycodegen "datatype" datatype_tycodegen 
-  #> DatatypeHooks.add (fold add_datatype_case_const)
-  #> DatatypeHooks.add (fold add_datatype_case_defs)
+  #> add_tycodegen "datatype" datatype_tycodegen
+  #> DatatypePackage.add_interpretator (fold add_datatype_case_const)
+  #> DatatypePackage.add_interpretator (fold add_datatype_case_defs)
 
 val setup_hooks =
-  add_codetypes_hook_bootstrap codetype_hook
-  #> add_codetypes_hook_bootstrap eq_hook
+  add_codetypes_hook codetype_hook
+  #> add_codetypes_hook eq_hook
 
 
 end;