src/HOL/Induct/ABexp.thy
changeset 58249 180f1b3508ed
parent 46914 c2ca2c3d23a6
child 58310 91ea607a34d8
--- a/src/HOL/Induct/ABexp.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Induct/ABexp.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
 imports Main
 begin
 
-datatype 'a aexp =
+datatype_new 'a aexp =
     IF "'a bexp"  "'a aexp"  "'a aexp"
   | Sum "'a aexp"  "'a aexp"
   | Diff "'a aexp"  "'a aexp"