src/HOL/HOLCF/IOA/ABP/Abschannel.thy
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 58880 0baae4311a9f
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
 imports IOA Action Lemmas
 begin
 
-datatype_new 'a abs_action = S 'a | R 'a
+datatype 'a abs_action = S 'a | R 'a
 
 
 (**********************************************************