diff -r 967444d352b8 -r 9764b994a421 src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Wed Sep 03 00:06:19 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Wed Sep 03 00:06:21 2014 +0200
@@ -132,7 +132,7 @@
 
 subsection {* AVL Trees *}
 
-datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
+datatype_new 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
 
 primrec set_of :: "'a tree \<Rightarrow> 'a set"
 where
@@ -221,7 +221,7 @@
 
 declare is_ord.simps(1)[code] is_ord_mkt[code]
 
-subsubsection {* Invalid Lemma due to typo in lbal *}
+subsubsection {* Invalid Lemma due to typo in @{const l_bal} *}
 
 lemma is_ord_l_bal:
  "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"