src/HOLCF/ex/Loop.thy

--- a/src/HOLCF/ex/Loop.thy	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOLCF/ex/Loop.thy	Wed Nov 03 15:03:16 2010 -0700
@@ -47,8 +47,7 @@
 apply simp
 apply (rule allI)
 apply (rule trans)
-apply (subst while_unfold)
-apply (rule_tac [2] refl)
+apply (rule while_unfold)
 apply (subst iterate_Suc2)
 apply (rule trans)
 apply (erule_tac [2] spec)
@@ -57,9 +56,7 @@
 apply simp
 apply (subst while_unfold)
 apply (rule_tac s = "UU" and t = "b$UU" in ssubst)
-apply (erule flat_codom [THEN disjE])
-apply assumption
-apply (erule spec)
+apply (erule strictI)
 apply simp
 apply simp
 apply simp