diff -r 9cb98d34f593 -r e88e980ed735 src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Sun Jan 15 14:55:30 2012 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Sun Jan 15 18:55:27 2012 +0100
@@ -155,7 +155,7 @@
 lemma (in Semilat) le_iff_plus_unchanged: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (x \<squnion>\<^sub>f y = y)"
 (*<*)
 apply (rule iffI)
- apply (blast intro: antisym_r refl_r lub ub2)
+ apply (blast intro: antisym_r lub ub2)
 apply (erule subst)
 apply simp
 done
@@ -164,7 +164,7 @@
 lemma (in Semilat) le_iff_plus_unchanged2: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (y \<squnion>\<^sub>f x = y)"
 (*<*)
 apply (rule iffI)
- apply (blast intro: order_antisym lub order_refl ub1)
+ apply (blast intro: order_antisym lub ub1)
 apply (erule subst)
 apply simp
 done