src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

    calls: rec_call list,
    rec_thm: thm};
 
 type rec_spec =
   {recx: term,
-   fp_nesting_map_idents: thm list,
+   fp_nesting_map_ident0s: thm list,
    fp_nesting_map_comps: thm list,
    ctr_specs: rec_ctr_spec list};
 
 type basic_lfp_sugar =
   {T: typ,

 
 fun rec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
-    val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_idents, fp_nesting_map_comps,
+    val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_ident0s, fp_nesting_map_comps,
          common_induct, n2m, lthy) =
       get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0;
 
     val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
 

         rec_thms;
 
     fun mk_spec ctr_offset
         ({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) =
       {recx = mk_co_rec thy Least_FP (substAT T) perm_Cs' recx,
-       fp_nesting_map_idents = fp_nesting_map_idents, fp_nesting_map_comps = fp_nesting_map_comps,
+       fp_nesting_map_ident0s = fp_nesting_map_ident0s, fp_nesting_map_comps = fp_nesting_map_comps,
        ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
   in
     ((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, common_induct, inducts), lthy)
   end;
 

   in
     map (find [] rhs_term) ctr_args
     |> (fn [] => NONE | callss => SOME (ctr, callss))
   end;
 
-fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx =
+fun mk_primrec_tac ctxt num_extra_args map_ident0s map_comps fun_defs recx =
   unfold_thms_tac ctxt fun_defs THEN
   HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
-  unfold_thms_tac ctxt (nested_simps ctxt @ map_comps @ map_idents) THEN
+  unfold_thms_tac ctxt (nested_simps ctxt @ map_ident0s @ map_comps) THEN
   HEADGOAL (rtac refl);
 
 fun prepare_primrec nonexhaustive fixes specs lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;

         raise PRIMREC ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^
           " is not a constructor in left-hand side", [user_eqn])) eqns_data;
 
     val defs = build_defs lthy nonexhaustive bs mxs funs_data rec_specs has_call;
 
-    fun prove lthy' def_thms' ({ctr_specs, fp_nesting_map_idents, fp_nesting_map_comps, ...}
+    fun prove lthy' def_thms' ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps, ...}
         : rec_spec) (fun_data : eqn_data list) =
       let
         val js =
           find_indices (op = o pairself (fn {fun_name, ctr, ...} => (fun_name, ctr)))
             fun_data eqns_data;

         val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
           |> fst
           |> map_filter (try (fn (x, [y]) =>
             (#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
           |> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) =>
-              mk_primrec_tac lthy' num_extra_args fp_nesting_map_idents fp_nesting_map_comps
+              mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
                 def_thms rec_thm
               |> K |> Goal.prove_sorry lthy' [] [] user_eqn
               (* for code extraction from proof terms: *)
               |> singleton (Proof_Context.export lthy' lthy)
               |> Thm.name_derivation (Sign.full_name thy (Binding.name fun_name) ^