--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Mar 13 20:04:24 2012 +0100
@@ -83,7 +83,7 @@
fun mk_const (b, T, _) = Const (Sign.full_name thy b, T)
val consts = map mk_const decls
fun mk_def c (b, t, _) =
- (Binding.suffix_name "_def" b, Logic.mk_equals (c, t))
+ (Thm.def_binding b, Logic.mk_equals (c, t))
val defs = map2 mk_def consts specs
val (def_thms, thy) =
Global_Theory.add_defs false (map Thm.no_attributes defs) thy