1.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Tue Mar 13 17:17:52 2012 +0000
     1.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Tue Mar 13 20:04:24 2012 +0100
     1.3 @@ -134,7 +134,7 @@
     1.4          Abs ("t", Term.itselfT newT,
     1.5            mk_capply (@{const liftdefl_of}, defl_const newT $ Logic.mk_type newT)))
     1.6  
     1.7 -    val name_def = Binding.suffix_name "_def" name
     1.8 +    val name_def = Thm.def_binding name
     1.9      val emb_bind = (Binding.prefix_name "emb_" name_def, [])
    1.10      val prj_bind = (Binding.prefix_name "prj_" name_def, [])
    1.11      val defl_bind = (Binding.prefix_name "defl_" name_def, [])