src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML

       | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
   in
     massage_call
   end;
 
-fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
-  let
-    val thy = Proof_Context.theory_of lthy;
+fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
+  let
+    val thy = Proof_Context.theory_of lthy0;
 
     val ((missing_arg_Ts, perm0_kks,
           fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...},
-            co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy') =
-      nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy;
+            co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy) =
+      nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy0;
 
     val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
 
     val indices = map #index fp_sugars;
     val perm_indices = map #index perm_fp_sugars;

       {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
        nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
        nested_map_comps = map map_comp_of_bnf nested_bnfs,
        ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
   in
-    ((is_some lfp_sugar_thms, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms),
-     lthy')
+    ((is_some lfp_sugar_thms, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms), lthy)
   end;
 
 val undef_const = Const (@{const_name undefined}, dummyT);
 
 fun permute_args n t =