src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

     val nn = length perm_ctrss;
     val kks = 0 upto nn - 1;
 
     val perm_ctr_offsets = map (fn kk => Integer.sum (map length (take kk perm_ctrss))) kks;
 
-    val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
+    val perm_fpTs = map #T perm_basic_lfp_sugars;
     val perm_Cs = map #C perm_basic_lfp_sugars;
     val perm_fun_arg_Tssss = map #fun_arg_Tsss perm_basic_lfp_sugars;
 
     fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
     fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
 
     val inducts = unpermute0 (conj_dests nn common_induct);
 
-    val lfpTs = unpermute perm_lfpTs;
+    val fpTs = unpermute perm_fpTs;
     val Cs = unpermute perm_Cs;
     val ctr_offsets = unpermute perm_ctr_offsets;
 
-    val As_rho = tvar_subst thy (take nn0 lfpTs) arg_Ts;
+    val As_rho = tvar_subst thy (take nn0 fpTs) arg_Ts;
     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;