--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Mar 13 20:04:24 2012 +0100
@@ -394,7 +394,7 @@
fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T);
val consts = map mk_const decls;
fun mk_def c (b, t, mx) =
- (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;