1.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Tue Nov 12 13:47:24 2013 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Tue Nov 12 13:47:24 2013 +0100
     1.3 @@ -86,16 +86,50 @@
     1.4  
     1.5  val info_of_case = Symtab.lookup o #cases o Data.get;
     1.6  
     1.7 -fun register (dt_infos : (string * Datatype_Aux.info) list) =
     1.8 +fun ctrs_of_exhaust exhaust =
     1.9 +  Logic.strip_imp_prems (prop_of exhaust) |>
    1.10 +  map (head_of o snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o the_single
    1.11 +    o Logic.strip_assums_hyp);
    1.12 +
    1.13 +fun case_of_case_rewrite case_rewrite =
    1.14 +  head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of case_rewrite))));
    1.15 +
    1.16 +fun ctr_sugar_of_info ({exhaust, nchotomy, inject, distinct, case_rewrites, case_cong,
    1.17 +    weak_case_cong, split, split_asm, ...} : Datatype_Aux.info) =
    1.18 +  {ctrs = ctrs_of_exhaust exhaust,
    1.19 +   casex = case_of_case_rewrite (hd case_rewrites),
    1.20 +   discs = [],
    1.21 +   selss = [],
    1.22 +   exhaust = exhaust,
    1.23 +   nchotomy = nchotomy,
    1.24 +   injects = inject,
    1.25 +   distincts = distinct,
    1.26 +   case_thms = case_rewrites,
    1.27 +   case_cong = case_cong,
    1.28 +   weak_case_cong = weak_case_cong,
    1.29 +   split = split,
    1.30 +   split_asm = split_asm,
    1.31 +   disc_thmss = [],
    1.32 +   discIs = [],
    1.33 +   sel_thmss = [],
    1.34 +   disc_exhausts = [],
    1.35 +   sel_exhausts = [],
    1.36 +   collapses = [],
    1.37 +   expands = [],
    1.38 +   sel_splits = [],
    1.39 +   sel_split_asms = [],
    1.40 +   case_conv_ifs = []};
    1.41 +
    1.42 +fun register dt_infos =
    1.43    Data.map (fn {types, constrs, cases} =>
    1.44      {types = types |> fold Symtab.update dt_infos,
    1.45       constrs = constrs |> fold (fn (constr, dtname_info) =>
    1.46           Symtab.map_default (constr, []) (cons dtname_info))
    1.47         (maps (fn (dtname, info as {descr, index, ...}) =>
    1.48 -          map (rpair (dtname, info) o fst)
    1.49 -            (#3 (the (AList.lookup op = descr index)))) dt_infos),
    1.50 +          map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos),
    1.51       cases = cases |> fold Symtab.update
    1.52 -       (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)});
    1.53 +       (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #>
    1.54 +  fold (fn (key, info) => Ctr_Sugar.register_ctr_sugar_global key (ctr_sugar_of_info info)) dt_infos;
    1.55  
    1.56  
    1.57  (* complex queries *)

     2.1 --- a/src/HOL/Tools/ctr_sugar.ML	Tue Nov 12 13:47:24 2013 +0100
     2.2 +++ b/src/HOL/Tools/ctr_sugar.ML	Tue Nov 12 13:47:24 2013 +0100
     2.3 @@ -37,6 +37,7 @@
     2.4    val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
     2.5    val ctr_sugars_of: Proof.context -> ctr_sugar list
     2.6    val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
     2.7 +  val register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
     2.8  
     2.9    val rep_compat_prefix: string
    2.10  
    2.11 @@ -143,6 +144,9 @@
    2.12    Local_Theory.declaration {syntax = false, pervasive = true}
    2.13      (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
    2.14  
    2.15 +fun register_ctr_sugar_global key ctr_sugar =
    2.16 +  Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
    2.17 +
    2.18  val rep_compat_prefix = "new";
    2.19  
    2.20  val isN = "is_";