--- a/src/HOL/Bali/Example.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Bali/Example.thy Thu Sep 11 19:32:36 2014 +0200
@@ -66,9 +66,9 @@
section "type and expression names"
(** unfortunately cannot simply instantiate tnam **)
-datatype_new tnam' = HasFoo' | Base' | Ext' | Main'
-datatype_new vnam' = arr' | vee' | z' | e'
-datatype_new label' = lab1'
+datatype tnam' = HasFoo' | Base' | Ext' | Main'
+datatype vnam' = arr' | vee' | z' | e'
+datatype label' = lab1'
axiomatization
tnam' :: "tnam' \<Rightarrow> tnam" and