src/HOL/Bali/DefiniteAssignmentCorrect.thy

       have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))" 
         by simp
       also
       from ass_ok
       have "\<dots> \<subseteq> dom (locals (store (assign f v s2)))"
-        by (rule dom_locals_assign_mono)
+        by (rule dom_locals_assign_mono [where f = f])
       finally show ?thesis by simp
     next
       case False
       with `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2`
       have "s2=s1"