diff -r e6e1ec6d5c1c -r a7ca72710dfe src/HOL/Bali/WellType.thy --- a/src/HOL/Bali/WellType.thy Mon Feb 27 17:39:34 2012 +0100 +++ b/src/HOL/Bali/WellType.thy Mon Feb 27 17:40:59 2012 +0100 @@ -546,7 +546,7 @@ then show ?thesis by blast next case False then show ?thesis - by (auto simp add: invmode_def split: split_if_asm) + by (auto simp add: invmode_def) qed qed