src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

     (Attrib.binding * string) list -> local_theory -> local_theory;
   val add_primcorec_cmd: bool ->
     (binding * string option * mixfix) list * (Attrib.binding * string) list -> Proof.context ->
     Proof.state
 end;
-
-(* TODO:
-     - error handling for indirect calls
-*)
 
 structure BNF_FP_Rec_Sugar : BNF_FP_REC_SUGAR =
 struct
 
 open BNF_Util

         primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy' ctr) ^
           " is not a constructor in left-hand side") user_eqn) eqns_data end;
 
     val defs = build_defs lthy' bs funs_data rec_specs get_indices;
 
-    fun prove def_thms' {ctr_specs, nested_map_id's, nested_map_comps, ...} induct_thm fun_data
+    fun prove def_thms' {ctr_specs, nested_map_idents, nested_map_comps, ...} induct_thm fun_data
         lthy =
       let
         val fun_name = #fun_name (hd fun_data);
         val def_thms = map (snd o snd) def_thms';
         val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
           |> fst
           |> map_filter (try (fn (x, [y]) =>
             (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
           |> map (fn (user_eqn, num_extra_args, rec_thm) =>
-            mk_primrec_tac lthy num_extra_args nested_map_id's nested_map_comps def_thms rec_thm
+            mk_primrec_tac lthy num_extra_args nested_map_idents nested_map_comps def_thms rec_thm
             |> K |> Goal.prove lthy [] [] user_eqn)
 
         val notes =
           [(inductN, if actual_nn > 1 then [induct_thm] else [], []),
            (simpsN, simp_thms, simp_attrs)]