rationalized data structure

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 11:58:18 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 12:35:02 2013 +0200
@@ -8,7 +8,8 @@
 signature BNF_FP_DEF_SUGAR =
 sig
   type fp_sugar =
-    {lfp: bool,
+    {T: typ,
+     lfp: bool,
      index: int,
      pre_bnfs: BNF_Def.bnf list,
      fp_res: BNF_FP_Util.fp_result,
@@ -73,7 +74,8 @@
 val EqN = "Eq_";
 
 type fp_sugar =
-  {lfp: bool,
+  {T: typ,
+   lfp: bool,
    index: int,
    pre_bnfs: bnf list,
    fp_res: fp_result,
@@ -83,13 +85,13 @@
    un_fold_thmss: thm list list,
    co_rec_thmss: thm list list};
 
-fun eq_fp_sugar ({lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
-    {lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
-  lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
+fun eq_fp_sugar ({T = T1, lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
+    {T = T2, lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
+  T1 = T2 andalso lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
 
-fun morph_fp_sugar phi {lfp, index, pre_bnfs, fp_res, ctr_sugars, un_folds, co_recs, un_fold_thmss,
-    co_rec_thmss} =
-  {lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
+fun morph_fp_sugar phi {T, lfp, index, pre_bnfs, fp_res, ctr_sugars, un_folds, co_recs,
+    un_fold_thmss, co_rec_thmss} =
+  {T = Morphism.typ phi T, lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
    fp_res = morph_fp_result phi fp_res, ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
    un_folds = map (Morphism.term phi) un_folds, co_recs = map (Morphism.term phi) co_recs,
    un_fold_thmss = map (map (Morphism.thm phi)) un_fold_thmss,
@@ -109,13 +111,13 @@
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar)));
 
-fun register_fp_sugars lfp pre_bnfs (fp_res as {ctors, ...}) ctr_sugars un_folds co_recs
+fun register_fp_sugars lfp pre_bnfs (fp_res as {Ts, ...}) ctr_sugars un_folds co_recs
     un_fold_thmss co_rec_thmss lthy =
   (0, lthy)
-  |> fold (fn ctor => fn (kk, lthy) => (kk + 1,
-    register_fp_sugar (fp_name_of_ctor ctor) {lfp = lfp, index = kk,
-      pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_sugars = ctr_sugars, un_folds = un_folds,
-      co_recs = co_recs, un_fold_thmss = un_fold_thmss, co_rec_thmss = co_rec_thmss} lthy)) ctors
+  |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
+    register_fp_sugar s {T = T, lfp = lfp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res,
+      ctr_sugars = ctr_sugars, un_folds = un_folds, co_recs = co_recs,
+      un_fold_thmss = un_fold_thmss, co_rec_thmss = co_rec_thmss} lthy)) Ts
   |> snd;
 
 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
@@ -904,7 +906,7 @@
     val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
            folds = fp_folds0, recs = fp_recs0, induct = fp_induct, strong_induct = fp_strong_induct,
            dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss,
-           rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms}, lthy)) =
+           rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms, ...}, lthy)) =
       fp_bnf construct_fp fp_bs mixfixes map_bs rel_bs set_bss (map dest_TFree unsorted_As) fp_eqs
         no_defs_lthy0;
 
@@ -1315,7 +1317,7 @@
       end;
 
     fun derive_and_note_coinduct_unfold_corec_thms_for_types
-        ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
+        ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
           (unfolds, corecs, unfold_defs, corec_defs)), lthy) =
       let
         val ((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms,

--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 11:58:18 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 12:35:02 2013 +0200
@@ -9,7 +9,8 @@
 signature BNF_FP_UTIL =
 sig
   type fp_result =
-    {bnfs: BNF_Def.bnf list,
+    {Ts: typ list,
+     bnfs: BNF_Def.bnf list,
      ctors: term list,
      dtors: term list,
      folds: term list,
@@ -25,7 +26,6 @@
      fold_thms: thm list,
      rec_thms: thm list}
 
-  val fp_name_of_ctor: term -> string
   val morph_fp_result: morphism -> fp_result -> fp_result
   val eq_fp_result: fp_result * fp_result -> bool
 
@@ -179,7 +179,8 @@
 open BNF_Util
 
 type fp_result =
-  {bnfs: BNF_Def.bnf list,
+  {Ts: typ list,
+   bnfs: BNF_Def.bnf list,
    ctors: term list,
    dtors: term list,
    folds: term list,
@@ -195,11 +196,10 @@
    fold_thms: thm list,
    rec_thms: thm list};
 
-val fp_name_of_ctor = fst o dest_Type o range_type o fastype_of;
-
-fun morph_fp_result phi {bnfs, ctors, dtors, folds, recs, induct, strong_induct, dtor_ctors,
+fun morph_fp_result phi {Ts, bnfs, ctors, dtors, folds, recs, induct, strong_induct, dtor_ctors,
     ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, fold_thms, rec_thms} =
-  {bnfs = map (morph_bnf phi) bnfs,
+  {Ts = map (Morphism.typ phi) Ts,
+   bnfs = map (morph_bnf phi) bnfs,
    ctors = map (Morphism.term phi) ctors,
    dtors = map (Morphism.term phi) dtors,
    folds = map (Morphism.term phi) folds,

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 11:58:18 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 12:35:02 2013 +0200
@@ -3029,7 +3029,7 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ({bnfs = Jbnfs, ctors = ctors, dtors = dtors, folds = unfolds, recs = corecs,
+    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, folds = unfolds, recs = corecs,
       induct = dtor_coinduct_thm, strong_induct = dtor_strong_coinduct_thm,
       dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
       map_thms = folded_dtor_map_thms, set_thmss = folded_dtor_set_thmss',

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 11:58:18 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 12:35:02 2013 +0200
@@ -1852,7 +1852,7 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ({bnfs = Ibnfs, ctors = ctors, dtors = dtors, folds = folds, recs = recs,
+    ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, folds = folds, recs = recs,
       induct = ctor_induct_thm, strong_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
       ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms,
       set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, fold_thms = ctor_fold_thms,