--- a/src/HOL/Induct/Comb.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Induct/Comb.thy Tue Sep 09 20:51:36 2014 +0200
@@ -20,7 +20,7 @@
text {* Datatype definition of combinators @{text S} and @{text K}. *}
-datatype comb = K
+datatype_new comb = K
| S
| Ap comb comb (infixl "##" 90)