diff -r c5232e6fb10b -r 3fb16bed5d6c src/HOL/Data_Structures/Trie_Map.thy
--- a/src/HOL/Data_Structures/Trie_Map.thy	Tue Sep 24 17:36:14 2019 +0200
+++ b/src/HOL/Data_Structures/Trie_Map.thy	Wed Sep 25 17:22:57 2019 +0200
@@ -21,10 +21,10 @@
 
 However, the development below works verbatim for any map implementation, eg \<open>Tree_Map\<close>,
 and not just \<open>RBT_Map\<close>, except for the termination lemma \<open>lookup_size\<close>.\<close>
-
+term size_tree
 lemma lookup_size[termination_simp]:
   fixes t :: "('a::linorder * 'a trie_map) rbt"
-  shows "lookup t a = Some b \<Longrightarrow> size b < Suc (size_tree (\<lambda>ab. Suc (size (snd ab))) (\<lambda>x. 0) t)"
+  shows "lookup t a = Some b \<Longrightarrow> size b < Suc (size_tree (\<lambda>ab. Suc(Suc (size (snd(fst ab))))) t)"
 apply(induction t a rule: lookup.induct)
 apply(auto split: if_splits)
 done