src/HOL/ex/Fundefs.thy

--- a/src/HOL/ex/Fundefs.thy	Mon Dec 17 18:37:49 2007 +0100
+++ b/src/HOL/ex/Fundefs.thy	Mon Dec 17 18:38:28 2007 +0100
@@ -279,7 +279,7 @@
   Leaf 'a 
   | Branch "'a tree list"
 
-lemma lem:"x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"
+lemma lem:"x \<in> set l \<Longrightarrow> size x < Suc (list_size size l)"
 by (induct l, auto)
 
 function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"