# HG changeset patch
# User haftmann
# Date 1274454976 -7200
# Node ID 8f9f3d61ca8c20b02302a70be62c9fdb461949b2
# Parent  609ad88a94fca9dae8c3f57b000f44cf5424b92d
adjusted to changes in Mapping.thy

diff -r 609ad88a94fc -r 8f9f3d61ca8c src/HOL/ex/Execute_Choice.thy
--- 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))"