1.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Wed Jul 02 17:34:45 2014 +0200
     1.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Wed Jun 11 14:24:23 2014 +1000
     1.3 @@ -367,6 +367,7 @@
     1.4           A \<notin> bad;  evs \<in> zg |]
     1.5       ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
     1.6  apply clarify
     1.7 +apply hypsubst_thin
     1.8  apply (erule rev_mp)
     1.9  apply (erule rev_mp)
    1.10  apply (erule zg.induct)