changeset 18447 | da548623916a |
parent 18249 | 4398f0f12579 |
child 18576 | 8d98b7711e47 |
--- a/src/HOL/Bali/TypeSafe.thy Tue Dec 20 22:06:00 2005 +0100 +++ b/src/HOL/Bali/TypeSafe.thy Wed Dec 21 12:02:57 2005 +0100 @@ -1466,7 +1466,7 @@ next case (VNam vn) with EName el_in_list show ?thesis - by (auto simp add: dom_def dest: map_upds_cut_irrelevant) + by (auto simp add: not_Some_eq dom_def dest: map_upds_cut_irrelevant) qed qed qed