--- a/src/HOL/Data_Structures/AA_Set.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Data_Structures/AA_Set.thy Thu Feb 15 12:11:00 2018 +0100
@@ -193,7 +193,7 @@
lemma lvl_insert_incr_iff: "(lvl(insert a t) = lvl t + 1) \<longleftrightarrow>
- (EX l x r. insert a t = Node (lvl t + 1) l x r \<and> lvl l = lvl r)"
+ (\<exists>l x r. insert a 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)