src/HOL/Data_Structures/Lookup2.thy

--- a/src/HOL/Data_Structures/Lookup2.thy	Tue Sep 24 17:36:14 2019 +0200
+++ b/src/HOL/Data_Structures/Lookup2.thy	Wed Sep 25 17:22:57 2019 +0200
@@ -9,13 +9,13 @@
   Map_Specs
 begin
 
-fun lookup :: "('a::linorder * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
+fun lookup :: "(('a::linorder * 'b) * 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
 "lookup Leaf x = None" |
-"lookup (Node l (a,b) _ r) x =
+"lookup (Node l ((a,b), _) r) x =
   (case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"
 
 lemma lookup_map_of:
   "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
-by(induction t) (auto simp: map_of_simps split: option.split)
+by(induction t rule: tree2_induct) (auto simp: map_of_simps split: option.split)
 
 end