src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML

     val eqns = map mk_eqn projs
 
     (* register constant definitions *)
     val (fixdef_thms, thy) =
       (Global_Theory.add_defs false o map Thm.no_attributes)
-        (map (Binding.suffix_name "_def") binds ~~ eqns) thy
+        (map Thm.def_binding binds ~~ eqns) thy
 
     (* prove applied version of definitions *)
     fun prove_proj (lhs, rhs) =
       let
         val tac = rewrite_goals_tac fixdef_thms THEN (simp_tac beta_ss) 1

     : (term * thm) * theory =
   let
     val typ = Term.fastype_of rhs
     val (const, thy) = Sign.declare_const_global ((bind, typ), NoSyn) thy
     val eqn = Logic.mk_equals (const, rhs)
-    val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn)
+    val def = Thm.no_attributes (Thm.def_binding bind, eqn)
     val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy
   in
     ((const, def_thm), thy)
   end