more correct (!) types for recursive calls

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Oct 24 15:56:03 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Oct 24 18:37:54 2013 +0200
@@ -219,44 +219,33 @@
       val ctr_args = #ctr_args eqn_data;
 
       val calls = #calls ctr_spec;
-      val n_args = fold (curry (op +) o (fn Mutual_Rec _ => 2 | _ => 1)) calls 0;
+      val n_args = fold (Integer.add o (fn Mutual_Rec _ => 2 | _ => 1)) calls 0;
 
       val no_calls' = tag_list 0 calls
-        |> map_filter (try (apsnd (fn No_Rec n => n | Mutual_Rec (n, _) => n)));
+        |> map_filter (try (apsnd (fn No_Rec p => p | Mutual_Rec (p, _) => p)));
       val mutual_calls' = tag_list 0 calls
-        |> map_filter (try (apsnd (fn Mutual_Rec (_, n) => n)));
+        |> map_filter (try (apsnd (fn Mutual_Rec (_, p) => p)));
       val nested_calls' = tag_list 0 calls
-        |> map_filter (try (apsnd (fn Nested_Rec n => n)));
-
-      fun make_mutual_type _ = dummyT; (* FIXME? *)
-
-      val rec_res_type_list = map (fn (x :: _) => (#rec_type x, #res_type x)) funs_data;
-
-      fun make_nested_type (Type (Tname, Ts)) = Type (Tname, Ts |> map (fn T =>
-        let val maybe_res_type = AList.lookup (op =) rec_res_type_list T in
-          if is_some maybe_res_type
-          then HOLogic.mk_prodT (T, the maybe_res_type)
-          else make_nested_type T end))
-        | make_nested_type T = T;
+        |> map_filter (try (apsnd (fn Nested_Rec p => p)));
 
       val args = replicate n_args ("", dummyT)
         |> Term.rename_wrt_term t
         |> map Free
-        |> fold (fn (ctr_arg_idx, arg_idx) =>
+        |> fold (fn (ctr_arg_idx, (arg_idx, T)) =>
             nth_map arg_idx (K (nth ctr_args ctr_arg_idx)))
           no_calls'
-        |> fold (fn (ctr_arg_idx, arg_idx) =>
-            nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_mutual_type)))
+        |> fold (fn (ctr_arg_idx, (arg_idx, T)) =>
+            nth_map arg_idx (K (retype_free T (nth ctr_args ctr_arg_idx))))
           mutual_calls'
-        |> fold (fn (ctr_arg_idx, arg_idx) =>
-            nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_nested_type)))
+        |> fold (fn (ctr_arg_idx, (arg_idx, T)) =>
+            nth_map arg_idx (K (retype_free T (nth ctr_args ctr_arg_idx))))
           nested_calls';
 
       val fun_name_ctr_pos_list =
         map (fn (x :: _) => (#fun_name x, length (#left_args x))) funs_data;
       val get_ctr_pos = try (the o AList.lookup (op =) fun_name_ctr_pos_list) #> the_default ~1;
-      val mutual_calls = map (apfst (nth ctr_args) o apsnd (nth args)) mutual_calls';
-      val nested_calls = map (apfst (nth ctr_args) o apsnd (nth args)) nested_calls';
+      val mutual_calls = map (apfst (nth ctr_args) o apsnd (nth args o fst)) mutual_calls';
+      val nested_calls = map (apfst (nth ctr_args) o apsnd (nth args o fst)) nested_calls';
 
       val abstractions = args @ #left_args eqn_data @ #right_args eqn_data;
     in

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Oct 24 15:56:03 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Oct 24 18:37:54 2013 +0200
@@ -9,9 +9,9 @@
 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 |
@@ -99,9 +99,9 @@
 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 |
@@ -567,6 +567,7 @@
     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;
 
@@ -574,8 +575,8 @@
       | 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