src/HOL/ex/Execute_Choice.thy
changeset 37055 8f9f3d61ca8c
parent 36109 1028cf8c0d1b
child 37595 9591362629e3
--- a/src/HOL/ex/Execute_Choice.thy	Fri May 21 15:28:25 2010 +0200
+++ b/src/HOL/ex/Execute_Choice.thy	Fri May 21 17:16:16 2010 +0200
@@ -26,7 +26,7 @@
   case True then show ?thesis by (simp add: is_empty_def keys_def valuesum_def)
 next
   case False
-  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def expand_fun_eq mem_def)
+  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def expand_fun_eq mem_def keys_def)
   then have "(let l = SOME l. l \<in> dom (Mapping.lookup m) in
      the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
        (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"