--- a/src/HOL/HOLCF/FOCUS/Buffer.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/HOLCF/FOCUS/Buffer.thy Thu Sep 11 19:32:36 2014 +0200
@@ -25,10 +25,10 @@
typedecl D
-datatype_new
+datatype
M = Md D | Mreq ("\<bullet>")
-datatype_new
+datatype
State = Sd D | Snil ("\<currency>")
type_synonym