src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 17:57:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 18:17:13 2013 +0200
@@ -13,6 +13,7 @@
      index: int,
      pre_bnfs: BNF_Def.bnf list,
      nested_bnfs: BNF_Def.bnf list,
+     nesting_bnfs: BNF_Def.bnf list,
      fp_res: BNF_FP_Util.fp_result,
      ctr_defss: thm list list,
      ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
@@ -112,6 +113,7 @@
    index: int,
    pre_bnfs: bnf list,
    nested_bnfs: bnf list,
+   nesting_bnfs: bnf list,
    fp_res: fp_result,
    ctr_defss: thm list list,
    ctr_sugars: ctr_sugar list,
@@ -125,10 +127,11 @@
     {T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
   T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
 
-fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, fp_res, ctr_defss, ctr_sugars,
-    co_iterss, co_inducts, co_iter_thmsss} =
+fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
+    ctr_sugars, co_iterss, co_inducts, co_iter_thmsss} =
   {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
-    nested_bnfs = map (morph_bnf phi) nested_bnfs, fp_res = morph_fp_result phi fp_res,
+    nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+   fp_res = morph_fp_result phi fp_res,
    ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
    ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
    co_iterss = map (map (Morphism.term phi)) co_iterss,
@@ -157,13 +160,14 @@
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
 
-fun register_fp_sugars fp pre_bnfs nested_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars co_iterss
-    co_inducts co_iter_thmsss lthy =
+fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
+    ctr_sugars co_iterss co_inducts co_iter_thmsss lthy =
   (0, lthy)
   |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
     register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs,
-        nested_bnfs = nested_bnfs, fp_res = fp_res, ctr_defss = ctr_defss, ctr_sugars = ctr_sugars,
-        co_iterss = co_iterss, co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss}
+        nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res,
+        ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss,
+        co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss}
       lthy)) Ts
   |> snd;
 
@@ -1430,8 +1434,8 @@
       in
         lthy
         |> Local_Theory.notes (common_notes @ notes) |> snd
-        |> register_fp_sugars Least_FP pre_bnfs nested_bnfs fp_res ctr_defss ctr_sugars iterss
-          [induct_thm] (transpose [fold_thmss, rec_thmss])
+        |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
+          iterss [induct_thm] (transpose [fold_thmss, rec_thmss])
       end;
 
     fun derive_and_note_coinduct_coiters_thms_for_types
@@ -1489,8 +1493,9 @@
       in
         lthy
         |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
-        |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs fp_res ctr_defss ctr_sugars coiterss
-          [coinduct_thm, strong_coinduct_thm] (transpose [unfold_thmss, corec_thmss])
+        |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
+          ctr_sugars coiterss [coinduct_thm, strong_coinduct_thm]
+          (transpose [unfold_thmss, corec_thmss])
       end;
 
     val lthy'' = lthy'