src/HOL/HOLCF/IOA/NTP/Impl.thy
changeset 58270 16648edf16e3
parent 54742 7a86358a3c0b
child 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Tue Sep 09 20:51:36 2014 +0200
     1.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Tue Sep 09 20:51:36 2014 +0200
     1.3 @@ -347,7 +347,7 @@
     1.4    apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv3_def}]
     1.5                                 (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
     1.6    apply simp
     1.7 -  apply (erule_tac x = "m" in allE)
     1.8 +  apply (rename_tac m, erule_tac x = "m" in allE)
     1.9    apply simp
    1.10    done
    1.11