diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -152,7 +152,7 @@
 
 lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
 apply (tactic {* pair_tac @{context} "exec" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 done
 
@@ -173,14 +173,14 @@
 (* TL = UU *)
 apply (rule conjI)
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 (* TL = nil *)
 apply (rule conjI)
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_tac @{context} "x2" 1 *})
 apply (simp add: unlift_def)
 apply fast
 apply (simp add: unlift_def)
@@ -193,7 +193,7 @@
 apply (simp add: unlift_def)
 
 apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})