1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 18 07:36:38 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 18 07:46:00 2007 +0200
     1.3 @@ -17,12 +17,11 @@
     1.4      -> theory -> theory
     1.5    val codetype_hook: hook
     1.6    val eq_hook: hook
     1.7 -  val codetypes_dependency: theory -> (string * bool) list list
     1.8 -  val add_codetypes_hook_bootstrap: hook -> theory -> theory
     1.9 +  val add_codetypes_hook: hook -> theory -> theory
    1.10    val the_codetypes_mut_specs: theory -> (string * bool) list
    1.11      -> ((string * sort) list * (string * (bool * (string * typ list) list)) list)
    1.12    val get_codetypes_arities: theory -> (string * bool) list -> sort
    1.13 -    -> (string * (arity * term list)) list option
    1.14 +    -> (string * (arity * term list)) list
    1.15    val prove_codetypes_arities: tactic -> (string * bool) list -> sort
    1.16      -> (arity list -> (string * term list) list -> theory
    1.17        -> ((bstring * Attrib.src list) * term) list * theory)
    1.18 @@ -443,6 +442,11 @@
    1.19  
    1.20  (* abstraction over datatypes vs. type copies *)
    1.21  
    1.22 +fun get_spec thy (dtco, true) =
    1.23 +      (the o DatatypePackage.get_datatype_spec thy) dtco
    1.24 +  | get_spec thy (tyco, false) =
    1.25 +      TypecopyPackage.get_spec thy tyco;
    1.26 +
    1.27  fun codetypes_dependency thy =
    1.28    let
    1.29      val names =
    1.30 @@ -472,11 +476,6 @@
    1.31      |> map (AList.make (the o AList.lookup (op =) names))
    1.32    end;
    1.33  
    1.34 -fun get_spec thy (dtco, true) =
    1.35 -      (the o DatatypePackage.get_datatype_spec thy) dtco
    1.36 -  | get_spec thy (tyco, false) =
    1.37 -      TypecopyPackage.get_spec thy tyco;
    1.38 -
    1.39  local
    1.40    fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    1.41     of SOME _ => get_eq_datatype thy tyco
    1.42 @@ -506,7 +505,7 @@
    1.43  type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
    1.44    -> theory -> theory;
    1.45  
    1.46 -fun add_codetypes_hook_bootstrap hook thy =
    1.47 +fun add_codetypes_hook hook thy =
    1.48    let
    1.49      fun add_spec thy (tyco, is_dt) =
    1.50        (tyco, (is_dt, get_spec thy (tyco, is_dt)));
    1.51 @@ -517,8 +516,8 @@
    1.52    in
    1.53      thy
    1.54      |> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy))
    1.55 -    |> DatatypeHooks.add datatype_hook
    1.56 -    |> TypecopyPackage.add_hook typecopy_hook
    1.57 +    |> DatatypePackage.add_interpretator datatype_hook
    1.58 +    |> TypecopyPackage.add_interpretator typecopy_hook
    1.59    end;
    1.60  
    1.61  fun the_codetypes_mut_specs thy ([(tyco, is_dt)]) =
    1.62 @@ -572,11 +571,11 @@
    1.63          val ty = (tys' ---> Type (tyco, map TFree vs'));
    1.64        in list_comb (Const (c, ty), map Free ts) end;
    1.65    in
    1.66 -    map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css |> SOME
    1.67 -  end handle Class_Error => NONE;
    1.68 +    map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
    1.69 +  end;
    1.70  
    1.71  fun prove_codetypes_arities tac tycos sort f after_qed thy =
    1.72 -  case get_codetypes_arities thy tycos sort
    1.73 +  case try (get_codetypes_arities thy tycos) sort
    1.74     of NONE => thy
    1.75      | SOME insts => let
    1.76          fun proven (tyco, asorts, sort) =
    1.77 @@ -634,13 +633,13 @@
    1.78  
    1.79  val setup = 
    1.80    add_codegen "datatype" datatype_codegen
    1.81 -  #> add_tycodegen "datatype" datatype_tycodegen 
    1.82 -  #> DatatypeHooks.add (fold add_datatype_case_const)
    1.83 -  #> DatatypeHooks.add (fold add_datatype_case_defs)
    1.84 +  #> add_tycodegen "datatype" datatype_tycodegen
    1.85 +  #> DatatypePackage.add_interpretator (fold add_datatype_case_const)
    1.86 +  #> DatatypePackage.add_interpretator (fold add_datatype_case_defs)
    1.87  
    1.88  val setup_hooks =
    1.89 -  add_codetypes_hook_bootstrap codetype_hook
    1.90 -  #> add_codetypes_hook_bootstrap eq_hook
    1.91 +  add_codetypes_hook codetype_hook
    1.92 +  #> add_codetypes_hook eq_hook
    1.93  
    1.94  
    1.95  end;