--- a/src/HOL/Data_Structures/AA_Map.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Data_Structures/AA_Map.thy Thu Feb 15 12:11:00 2018 +0100
@@ -64,7 +64,7 @@
qed simp
lemma lvl_update_incr_iff: "(lvl(update a b t) = lvl t + 1) \<longleftrightarrow>
- (EX l x r. update a b t = Node (lvl t + 1) l x r \<and> lvl l = lvl r)"
+ (\<exists>l x r. update a b t = Node (lvl t + 1) l x r \<and> lvl l = lvl r)"
apply(cases t)
apply(auto simp add: skew_case split_case split: if_splits)
apply(auto split: tree.splits if_splits)