src/HOL/ex/Execute_Choice.thy

 
 lemma valuesum_rec_Mapping:
   shows [code]: "valuesum (Mapping []) = 0"
   and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (Mapping (x # xs))) in
     the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
-  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping)
+  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping null_def)
 
 text {*
   As a side effect the precondition disappears (but note this has nothing to do with choice!).
   The first equation deals with the uncritical empty case and can already be used for code generation.