# HG changeset patch
# User wenzelm
# Date 1357250432 -3600
# Node ID 32007a8db6bbe942ec709081dcefe16af1c6419c
# Parent  985c081a4f11daebb924110d21c5539f6cbdf4a3
avoid long enumeration of HO unifiers;

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