1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 11:55:45 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 12:40:58 2013 +0100
     1.3 @@ -16,8 +16,8 @@
     1.4      (BNF_FP_Def_Sugar.fp_sugar list
     1.5       * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
     1.6      * local_theory
     1.7 -  val pad_and_indexify_calls: BNF_FP_Def_Sugar.fp_sugar list -> int ->
     1.8 -    (term * term list list) list list -> term list list list list
     1.9 +  val indexify_callsss: BNF_FP_Def_Sugar.fp_sugar -> (term * term list list) list ->
    1.10 +    term list list list
    1.11    val nested_to_mutual_fps: BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
    1.12      (term * term list list) list list -> local_theory ->
    1.13      (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
    1.14 @@ -118,7 +118,7 @@
    1.15      xs ([], ([], []));
    1.16  
    1.17  fun key_of_fp_eqs fp fpTs fp_eqs =
    1.18 -  Type (fp_case fp "l" "g", fpTs @ maps (fn (z, T) => [TFree z, T]) fp_eqs);
    1.19 +  Type (fp_case fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs);
    1.20  
    1.21  (* TODO: test with sort constraints on As *)
    1.22  (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
    1.23 @@ -284,8 +284,6 @@
    1.24      map do_ctr ctrs
    1.25    end;
    1.26  
    1.27 -fun pad_and_indexify_calls fp_sugars0 = map2 indexify_callsss fp_sugars0 oo pad_list [];
    1.28 -
    1.29  fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
    1.30    let
    1.31      val qsoty = quote o Syntax.string_of_typ lthy;
    1.32 @@ -351,6 +349,8 @@
    1.33      val nn = length Ts;
    1.34      val kks = 0 upto nn - 1;
    1.35  
    1.36 +    val callssss0 = pad_list [] nn actual_callssss0;
    1.37 +
    1.38      val common_name = mk_common_name (map Binding.name_of actual_bs);
    1.39      val bs = pad_list (Binding.name common_name) nn actual_bs;
    1.40  
    1.41 @@ -359,10 +359,11 @@
    1.42  
    1.43      val perm_bs = permute bs;
    1.44      val perm_kks = permute kks;
    1.45 +    val perm_callssss0 = permute callssss0;
    1.46      val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
    1.47  
    1.48      val has_nested = exists (fn Type (_, ty_args) => ty_args <> ty_args0) Ts;
    1.49 -    val perm_callssss = pad_and_indexify_calls perm_fp_sugars0 nn actual_callssss0;
    1.50 +    val perm_callssss = map2 indexify_callsss perm_fp_sugars0 perm_callssss0;
    1.51  
    1.52      val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
    1.53  

     2.1 --- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Tue Nov 05 11:55:45 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Tue Nov 05 12:40:58 2013 +0100
     2.3 @@ -93,7 +93,7 @@
     2.4      val nn = length Ts;
     2.5      val get_indices = K [];
     2.6      val fp_sugars0 = if nn = 1 then [fp_sugar0] else map (lfp_sugar_of o fst o dest_Type) Ts;
     2.7 -    val callssss = pad_and_indexify_calls fp_sugars0 nn [];
     2.8 +    val callssss = map (fn fp_sugar0 => indexify_callsss fp_sugar0 []) fp_sugars0;
     2.9      val has_nested = nn > nn_fp;
    2.10  
    2.11      val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =