src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML

 *)
 
 signature BNF_FP_REC_SUGAR_UTIL =
 sig
   datatype rec_call =
-    No_Rec of int |
-    Mutual_Rec of int (*before*) * int (*after*) |
-    Nested_Rec of int
+    No_Rec of int * typ |
+    Mutual_Rec of (int * typ) (*before*) * (int * typ) (*after*) |
+    Nested_Rec of int * typ
 
   datatype corec_call =
     Dummy_No_Corec of int |
     No_Corec of int |
     Mutual_Corec of int (*stop?*) * int (*end*) * int (*continue*) |

 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 open BNF_FP_N2M_Sugar
 
 datatype rec_call =
-  No_Rec of int |
-  Mutual_Rec of int * int |
-  Nested_Rec of int;
+  No_Rec of int * typ |
+  Mutual_Rec of (int * typ) * (int * typ) |
+  Nested_Rec of int * typ;
 
 datatype corec_call =
   Dummy_No_Corec of int |
   No_Corec of int |
   Mutual_Corec of int * int * int |

     val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
 
     val substA = Term.subst_TVars As_rho;
     val substAT = Term.typ_subst_TVars As_rho;
     val substCT = Term.typ_subst_TVars Cs_rho;
+    val substACT = substAT o substCT;
 
     val perm_Cs' = map substCT perm_Cs;
 
     fun offset_of_ctr 0 _ = 0
       | offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) =
         length ctrs + offset_of_ctr (n - 1) ctr_sugars;
 
-    fun call_of [i] [T] = (if exists_subtype_in Cs T then Nested_Rec else No_Rec) i
-      | call_of [i, i'] _ = Mutual_Rec (i, i');
+    fun call_of [i] [T] = (if exists_subtype_in Cs T then Nested_Rec else No_Rec) (i, substACT T)
+      | call_of [i, i'] [T, T'] = Mutual_Rec ((i, substACT T), (i', substACT T'));
 
     fun mk_ctr_spec ctr offset fun_arg_Tss rec_thm =
       let
         val (fun_arg_hss, _) = indexedd fun_arg_Tss 0;
         val fun_arg_hs = flat_rec_arg_args fun_arg_hss;