
diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Bali/Example.thy
--- 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




