--- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy Tue Sep 09 20:51:36 2014 +0200
@@ -89,7 +89,7 @@
apply (simp add: hom_ioas)
apply (blast dest!: add_leD1 [THEN leD])
-apply (case_tac "m = hd (sq (sen (s)))")
+apply (rename_tac m, case_tac "m = hd (sq (sen (s)))")
apply force
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy Tue Sep 09 20:51:36 2014 +0200
@@ -347,7 +347,7 @@
apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv3_def}]
(@{thm raw_inv3} RS @{thm invariantE})] 1 *})
apply simp
- apply (erule_tac x = "m" in allE)
+ apply (rename_tac m, erule_tac x = "m" in allE)
apply simp
done
--- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy Tue Sep 09 20:51:36 2014 +0200
@@ -53,7 +53,7 @@
apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
apply fast
txt {* FREE *}
-apply (rule_tac x = " (used - {nat},c) " in exI)
+apply (rename_tac nat, rule_tac x = " (used - {nat},c) " in exI)
apply simp
apply (rule transition_is_ex)
apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
--- a/src/HOL/Induct/Common_Patterns.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Induct/Common_Patterns.thy Tue Sep 09 20:51:36 2014 +0200
@@ -224,7 +224,7 @@
text {*
The pack of induction rules for this datatype is: @{thm [display]
- foo_bar_bazar.inducts [no_vars]}
+ foo.induct [no_vars] bar.induct [no_vars] bazar.induct [no_vars]}
This corresponds to the following basic proof pattern:
*}