fixed infinite loops in 'register' functions + more uniform API

--- a/src/HOL/Inductive.thy	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Inductive.thy	Fri Sep 05 00:41:01 2014 +0200
@@ -273,7 +273,7 @@
 
 ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
 ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
-ML_file "Tools/Old_Datatype/old_datatype_data.ML" setup Old_Datatype_Data.setup
+ML_file "Tools/Old_Datatype/old_datatype_data.ML"
 ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
 ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
 ML_file "Tools/Old_Datatype/old_primrec.ML"

--- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -1532,7 +1532,8 @@
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)));
 
-fun register_bnf key bnf = register_bnf_raw key bnf #> interpret_bnf bnf;
+fun register_bnf key bnf =
+  register_bnf_raw key bnf #> interpret_bnf bnf;
 
 fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs =
   (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -237,7 +237,7 @@
     fp_sugars;
 
 fun register_fp_sugars fp_sugars =
-  register_fp_sugars fp_sugars #> interpret_fp_sugars fp_sugars;
+  register_fp_sugars_raw fp_sugars #> interpret_fp_sugars fp_sugars;
 
 fun interpret_bnfs_register_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
     live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -352,12 +352,11 @@
     Type (T_name, _) =>
     (case Ctr_Sugar.ctr_sugar_of ctxt T_name of
       NONE => not_codatatype ctxt res_T
-    | SOME {ctrs, discs, selss, ...} =>
+    | SOME {T = fpT, ctrs, discs, selss, ...} =>
       let
         val thy = Proof_Context.theory_of ctxt;
 
-        val gfpT = body_type (fastype_of (hd ctrs));
-        val As_rho = tvar_subst thy [gfpT] [res_T];
+        val As_rho = tvar_subst thy [fpT] [res_T];
         val substA = Term.subst_TVars As_rho;
 
         fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels};
@@ -384,11 +383,11 @@
     val indices = map #fp_res_index fp_sugars;
     val perm_indices = map #fp_res_index perm_fp_sugars;
 
-    val perm_gfpTs = map #T perm_fp_sugars;
+    val perm_fpTs = map #T perm_fp_sugars;
     val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars;
 
     val nn0 = length res_Ts;
-    val nn = length perm_gfpTs;
+    val nn = length perm_fpTs;
     val kks = 0 upto nn - 1;
     val perm_ns' = map length perm_ctrXs_Tsss';
 
@@ -426,10 +425,10 @@
     val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss);
 
     val f_Tssss = unpermute perm_f_Tssss;
-    val gfpTs = unpermute perm_gfpTs;
+    val fpTs = unpermute perm_fpTs;
     val Cs = unpermute perm_Cs;
 
-    val As_rho = tvar_subst thy (take nn0 gfpTs) res_Ts;
+    val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts;
     val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts;
 
     val substA = Term.subst_TVars As_rho;

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -152,7 +152,7 @@
 
     val perm_ctr_offsets = map (fn kk => Integer.sum (map length (take kk perm_ctrss))) kks;
 
-    val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
+    val perm_fpTs = map #T perm_basic_lfp_sugars;
     val perm_Cs = map #C perm_basic_lfp_sugars;
     val perm_fun_arg_Tssss = map #fun_arg_Tsss perm_basic_lfp_sugars;
 
@@ -161,11 +161,11 @@
 
     val inducts = unpermute0 (conj_dests nn common_induct);
 
-    val lfpTs = unpermute perm_lfpTs;
+    val fpTs = unpermute perm_fpTs;
     val Cs = unpermute perm_Cs;
     val ctr_offsets = unpermute perm_ctr_offsets;
 
-    val As_rho = tvar_subst thy (take nn0 lfpTs) arg_Ts;
+    val As_rho = tvar_subst thy (take nn0 fpTs) arg_Ts;
     val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
 
     val substA = Term.subst_TVars As_rho;

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -8,7 +8,8 @@
 signature CTR_SUGAR =
 sig
   type ctr_sugar =
-    {ctrs: term list,
+    {T: typ,
+     ctrs: term list,
      casex: term,
      discs: term list,
      selss: term list list,
@@ -45,8 +46,10 @@
   val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
   val ctr_sugar_interpretation: string -> (ctr_sugar -> theory -> theory) ->
     (ctr_sugar -> local_theory -> local_theory) -> theory -> theory
-  val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
-  val default_register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
+  val interpret_ctr_sugar: ctr_sugar -> local_theory -> local_theory
+  val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory
+  val register_ctr_sugar: ctr_sugar -> local_theory -> local_theory
+  val default_register_ctr_sugar_global: ctr_sugar -> theory -> theory
 
   val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
   val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
@@ -84,7 +87,8 @@
 open Ctr_Sugar_Code
 
 type ctr_sugar =
-  {ctrs: term list,
+  {T: typ,
+   ctrs: term list,
    casex: term,
    discs: term list,
    selss: term list list,
@@ -111,11 +115,12 @@
    split_sel_asms: thm list,
    case_eq_ifs: thm list};
 
-fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
+fun morph_ctr_sugar phi {T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
     case_thms, case_cong, case_cong_weak, split, 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} =
-  {ctrs = map (Morphism.term phi) ctrs,
+  {T = Morphism.typ phi T,
+   ctrs = map (Morphism.term phi) ctrs,
    casex = Morphism.term phi casex,
    discs = map (Morphism.term phi) discs,
    selss = map (map (Morphism.term phi)) selss,
@@ -182,18 +187,22 @@
 fun ctr_sugar_interpretation name =
   Ctr_Sugar_Interpretation.interpretation name o with_transfer_ctr_sugar;
 
-fun register_ctr_sugar key ctr_sugar =
+val interpret_ctr_sugar = Ctr_Sugar_Interpretation.data;
+
+fun register_ctr_sugar_raw (ctr_sugar as {T = Type (s, _), ...}) =
   Local_Theory.declaration {syntax = false, pervasive = true}
-    (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar)))
-  #> Ctr_Sugar_Interpretation.data ctr_sugar;
+    (fn phi => Data.map (Symtab.update (s, morph_ctr_sugar phi ctr_sugar)));
 
-fun default_register_ctr_sugar_global key ctr_sugar thy =
+fun register_ctr_sugar ctr_sugar =
+  register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar ctr_sugar;
+
+fun default_register_ctr_sugar_global (ctr_sugar as {T = Type (s, _), ...}) thy =
   let val tab = Data.get (Context.Theory thy) in
-    if Symtab.defined tab key then
+    if Symtab.defined tab s then
       thy
     else
       thy
-      |> Context.theory_map (Data.put (Symtab.update_new (key, ctr_sugar) tab))
+      |> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab))
       |> Ctr_Sugar_Interpretation.data_global ctr_sugar
   end;
 
@@ -1025,7 +1034,7 @@
           |>> name_noted_thms fcT_name exhaustN;
 
         val ctr_sugar =
-          {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
+          {T = fcT, ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
            nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
            case_thms = case_thms, case_cong = case_cong_thm, case_cong_weak = case_cong_weak_thm,
            split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs,
@@ -1036,7 +1045,7 @@
            case_eq_ifs = case_eq_if_thms}
           |> morph_ctr_sugar (substitute_noted_thm noted);
       in
-        (ctr_sugar, lthy' |> register_ctr_sugar fcT_name ctr_sugar)
+        (ctr_sugar, lthy' |> register_ctr_sugar ctr_sugar)
       end;
   in
     (goalss, after_qed, lthy')

--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -25,7 +25,6 @@
   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 =
@@ -97,32 +96,35 @@
 
 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} =>
@@ -133,8 +135,7 @@
           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 *)
@@ -283,9 +284,7 @@
 
 (** setup theory **)
 
-val setup =
-  antiq_setup #>
-  Datatype_Interpretation.init;
+val _ = Theory.setup (antiq_setup #> Datatype_Interpretation.init);
 
 open Old_Datatype_Aux;
 

--- a/src/HOL/Tools/record.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/record.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -1781,14 +1781,15 @@
     end
   else thy;
 
-fun add_ctr_sugar T_name ctr sels exhaust inject sel_defs sel_thms =
-  Ctr_Sugar.default_register_ctr_sugar_global T_name
-    {ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels], exhaust = exhaust,
-     nchotomy = Drule.dummy_thm, injects = [inject], distincts = [], case_thms = [],
-     case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm, split = Drule.dummy_thm,
-     split_asm = Drule.dummy_thm, disc_defs = [], disc_thmss = [], discIs = [], sel_defs = sel_defs,
-     sel_thmss = [sel_thms], distinct_discsss = [], exhaust_discs = [], exhaust_sels = [],
-     collapses = [], expands = [], split_sels = [], split_sel_asms = [], case_eq_ifs = []};
+fun add_ctr_sugar ctr sels exhaust inject sel_defs sel_thms =
+  Ctr_Sugar.default_register_ctr_sugar_global
+    {T = body_type (fastype_of ctr), ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels],
+     exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject], distincts = [],
+     case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm,
+     split = Drule.dummy_thm, split_asm = Drule.dummy_thm, disc_defs = [], disc_thmss = [],
+     discIs = [], sel_defs = sel_defs, sel_thmss = [sel_thms], distinct_discsss = [],
+     exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [], split_sels = [],
+     split_sel_asms = [], case_eq_ifs = []};
 
 
 (* definition *)
@@ -2234,7 +2235,7 @@
       |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
       |> add_fieldext (extension_name, snd extension) names
       |> add_code ext_tyco vs extT ext simps' ext_inject
-      |> add_ctr_sugar ext_tyco (Const ext) sels cases_scheme' ext_inject sel_defs' sel_convs'
+      |> add_ctr_sugar (Const ext) sels cases_scheme' ext_inject sel_defs' sel_convs'
       |> Sign.restore_naming thy;
 
   in final_thy end;