tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

--- a/src/HOL/HOLCF/ex/Hoare.thy	Fri Jul 27 20:58:44 2012 +0200
+++ b/src/HOL/HOLCF/ex/Hoare.thy	Fri Jul 27 21:50:34 2012 +0200
@@ -267,7 +267,7 @@
 lemma hoare_lemma19:
   "(ALL k. (b1::'a->tr)$(iterate k$g$x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)"
 apply (rule flat_codom)
-apply (rule_tac t = "x1" in iterate_0 [THEN subst])
+apply (rule_tac t = "x" in iterate_0 [THEN subst])
 apply (erule spec)
 done