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