--- a/src/HOL/Induct/PropLog.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/PropLog.thy Thu Sep 11 19:32:36 2014 +0200
@@ -20,7 +20,7 @@
subsection {* The datatype of propositions *}
-datatype_new 'a pl =
+datatype 'a pl =
false |
var 'a ("#_" [1000]) |
imp "'a pl" "'a pl" (infixr "->" 90)