src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 63167 0909deb8059b
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -4,11 +4,11 @@
 
 subsection {* Lambda *}
 
-datatype_new type =
+datatype type =
     Atom nat
   | Fun type type    (infixr "\<Rightarrow>" 200)
 
-datatype_new dB =
+datatype dB =
     Var nat
   | App dB dB (infixl "\<degree>" 200)
   | Abs type dB