--- a/src/HOL/Decision_Procs/MIR.thy Tue Nov 27 10:56:31 2012 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Tue Nov 27 13:22:29 2012 +0100
@@ -5010,7 +5010,7 @@
from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp
from \<Upsilon>_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
from U_l UpU
- have Up_: "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
+ have "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 "
by (auto simp add: mult_pos_pos)
have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0"