# HG changeset patch
# User wenzelm
# Date 1343418634 -7200
# Node ID eaa36c0d620ae04740fe3d57f80bb84ce9e957a5
# Parent  04e1299311810a1dc5a4e9762fb4a7d5740bd15c
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

diff -r 04e129931181 -r eaa36c0d620a src/HOL/HOLCF/ex/Hoare.thy
--- 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