src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

         hd x |> #left_args |> length) funs_data;
   in
     (recs, ctr_poss)
     |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
     |> Syntax.check_terms lthy
-    |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.map_name Thm.def_name b, []), t))) bs mxs
+    |> map3 (fn b => fn mx => fn t =>
+      ((b, mx), ((Binding.conceal (Binding.map_name Thm.def_name b), []), t))) bs mxs
   end;
 
 fun find_rec_calls has_call (eqn_data : eqn_data) =
   let
     fun find (Abs (_, _, b)) ctr_arg = find b ctr_arg

   in
     map (list_comb o rpair corec_args) corecs
     |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
     |> map2 currys arg_Tss
     |> Syntax.check_terms lthy
-    |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.map_name Thm.def_name b, []), t))) bs mxs
+    |> map3 (fn b => fn mx => fn t =>
+      ((b, mx), ((Binding.conceal (Binding.map_name Thm.def_name b), []), t))) bs mxs
     |> rpair exclss'
   end;
 
 fun mk_real_disc_eqns fun_binding arg_Ts ({ctr_specs, ...} : corec_spec)
     (sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) =