src/HOL/UNITY/Comp/Counter.thy
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 58889 5b7a9633cfa8
--- a/src/HOL/UNITY/Comp/Counter.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/UNITY/Comp/Counter.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -13,7 +13,7 @@
 theory Counter imports "../UNITY_Main" begin
 
 (* Variables are names *)
-datatype_new name = C | c nat
+datatype name = C | c nat
 type_synonym state = "name=>int"
 
 primrec sum  :: "[nat,state]=>int" where