src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

             (list_comb (Const (name, T), args))))
         val lhs = Const (mode_cname, funT)
         val def = Logic.mk_equals (lhs, predterm)
         val ([definition], thy') = thy |>
           Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
-          Global_Theory.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
+          Global_Theory.add_defs false [((Binding.name (Thm.def_name mode_cbasename), def), [])]
         val ctxt' = Proof_Context.init_global thy'
         val rules as ((intro, elim), _) =
           create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
         in thy'
           |> set_function_name Pred name mode mode_cname