src/HOL/Library/Phantom_Type.thy
changeset 58249 180f1b3508ed
parent 52147 9943f8067f11
child 58310 91ea607a34d8
--- a/src/HOL/Library/Phantom_Type.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Library/Phantom_Type.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
 imports Main
 begin
 
-datatype ('a, 'b) phantom = phantom 'b
+datatype_new ('a, 'b) phantom = phantom 'b
 
 primrec of_phantom :: "('a, 'b) phantom \<Rightarrow> 'b" 
 where "of_phantom (phantom x) = x"