src/HOL/Tools/Old_Datatype/old_datatype_data.ML

   val get_constrs : theory -> string -> (string * typ) list option
   val mk_case_names_induct: descr -> attribute
   val mk_case_names_exhausts: descr -> string list -> attribute list
   val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
   val interpretation_data : config * string list -> theory -> theory
-  val setup: theory -> theory
 end;
 
 structure Old_Datatype_Data: OLD_DATATYPE_DATA =
 struct
 

 fun case_of_case_rewrite case_rewrite =
   head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of case_rewrite))));
 
 fun ctr_sugar_of_info ({exhaust, nchotomy, inject, distinct, case_rewrites, case_cong,
     case_cong_weak, split, split_asm, ...} : Old_Datatype_Aux.info) =
-  {ctrs = ctrs_of_exhaust exhaust,
-   casex = case_of_case_rewrite (hd case_rewrites),
-   discs = [],
-   selss = [],
-   exhaust = exhaust,
-   nchotomy = nchotomy,
-   injects = inject,
-   distincts = distinct,
-   case_thms = case_rewrites,
-   case_cong = case_cong,
-   case_cong_weak = case_cong_weak,
-   split = split,
-   split_asm = split_asm,
-   disc_defs = [],
-   disc_thmss = [],
-   discIs = [],
-   sel_defs = [],
-   sel_thmss = [],
-   distinct_discsss = [],
-   exhaust_discs = [],
-   exhaust_sels = [],
-   collapses = [],
-   expands = [],
-   split_sels = [],
-   split_sel_asms = [],
-   case_eq_ifs = []};
+  let val ctrs as ctr1 :: _ = ctrs_of_exhaust exhaust in
+    {T = body_type (fastype_of ctr1),
+     ctrs = ctrs,
+     casex = case_of_case_rewrite (hd case_rewrites),
+     discs = [],
+     selss = [],
+     exhaust = exhaust,
+     nchotomy = nchotomy,
+     injects = inject,
+     distincts = distinct,
+     case_thms = case_rewrites,
+     case_cong = case_cong,
+     case_cong_weak = case_cong_weak,
+     split = split,
+     split_asm = split_asm,
+     disc_defs = [],
+     disc_thmss = [],
+     discIs = [],
+     sel_defs = [],
+     sel_thmss = [],
+     distinct_discsss = [],
+     exhaust_discs = [],
+     exhaust_sels = [],
+     collapses = [],
+     expands = [],
+     split_sels = [],
+     split_sel_asms = [],
+     case_eq_ifs = []}
+  end;
 
 fun register dt_infos =
   Data.map (fn {types, constrs, cases} =>
     {types = types |> fold Symtab.update dt_infos,
      constrs = constrs |> fold (fn (constr, dtname_info) =>
          Symtab.map_default (constr, []) (cons dtname_info))
        (maps (fn (dtname, info as {descr, index, ...}) =>
           map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos),
      cases = cases |> fold Symtab.update
        (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #>
-  fold (fn (key, info) =>
-    Ctr_Sugar.default_register_ctr_sugar_global key (ctr_sugar_of_info info)) dt_infos;
+  fold (Ctr_Sugar.default_register_ctr_sugar_global o ctr_sugar_of_info o snd) dt_infos;
 
 
 (* complex queries *)
 
 fun the_spec thy dtco =

 
 
 
 (** setup theory **)
 
-val setup =
-  antiq_setup #>
-  Datatype_Interpretation.init;
+val _ = Theory.setup (antiq_setup #> Datatype_Interpretation.init);
 
 open Old_Datatype_Aux;
 
 end;