
diff -r 985c081a4f11 -r 32007a8db6bb src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Jan 03 22:12:18 2013 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Jan 03 23:00:32 2013 +0100
@@ -1467,7 +1467,7 @@
       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




