# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 16648edf16e3a4767edcea290dfb8cde40f7155d
# Parent  ad644790cbbb2b39f37cede8bf86af8c1a97752f
more porting to new datatypes

diff -r ad644790cbbb -r 16648edf16e3 src/HOL/HOLCF/IOA/NTP/Correctness.thy
--- 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
 
diff -r ad644790cbbb -r 16648edf16e3 src/HOL/HOLCF/IOA/NTP/Impl.thy
--- 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
 
diff -r ad644790cbbb -r 16648edf16e3 src/HOL/HOLCF/IOA/Storage/Correctness.thy
--- 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)
diff -r ad644790cbbb -r 16648edf16e3 src/HOL/Induct/Common_Patterns.thy
--- 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:
 *}