--- a/src/HOL/Nominal/Examples/CK_Machine.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy Thu Sep 11 19:32:36 2014 +0200
@@ -81,7 +81,7 @@
section {* Evaluation Contexts *}
-datatype_new ctx =
+datatype ctx =
Hole ("\<box>")
| CAPPL "ctx" "lam"
| CAPPR "lam" "ctx"