src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

     val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
           strong_coinduct_thms), lthy') =
       corec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy;
     val actual_nn = length bs;
     val corec_specs = take actual_nn corec_specs'; (*###*)
+    val ctr_specss = map #ctr_specs corec_specs;
 
     val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data
       |> partition_eq ((op =) o pairself #fun_name)
       |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
       |> map (sort ((op <) o pairself #ctr_no |> make_ord) o flat o snd);

                 |> Thm.close_derivation
                 |> pair ctr
                 |> single
             end;
 
-        fun prove_code disc_eqns sel_eqns ctr_alist {ctr_specs, ...} =
+        fun prove_code disc_eqns sel_eqns ctr_alist ctr_specs =
           let
             val (fun_name, fun_T, fun_args, maybe_rhs) =
               (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
                find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns)
               |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x))

                     let
                       val rhs = fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t)
                         maybe_ctr_conds_argss
                         (Const (@{const_name Code.abort}, @{typ String.literal} -->
                             (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
-                          @{term "STR []"} $ (* FIXME *)
+                          HOLogic.mk_literal fun_name $
                           absdummy @{typ unit} (incr_boundvars 1 lhs));
                     in SOME (rhs, rhs, map snd ctr_alist) end
                 end);
           in
             (case maybe_rhs_info of

         val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss exclssss sel_eqnss;
         val disc_thmss = map (map snd) disc_alists;
         val sel_thmss = map (map snd) sel_alists;
 
         val ctr_alists = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss
-          (map #ctr_specs corec_specs);
+          ctr_specss;
         val ctr_thmss = map (map snd) ctr_alists;
 
-        val code_thmss = map4 prove_code disc_eqnss sel_eqnss ctr_alists corec_specs;
+        val code_thmss = map4 prove_code disc_eqnss sel_eqnss ctr_alists ctr_specss;
 
         val simp_thmss = map2 append disc_thmss sel_thmss
 
         val common_name = mk_common_name fun_names;