src/HOL/Auth/Event.thy
changeset 27154 026f3db3f5c6
parent 24122 fc7f857d33c8
child 27225 b316dde851f5
     1.1 --- a/src/HOL/Auth/Event.thy	Wed Jun 11 18:02:00 2008 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Wed Jun 11 18:02:25 2008 +0200
     1.3 @@ -281,7 +281,7 @@
     1.4  ML
     1.5  {*
     1.6  val analz_mono_contra_tac = 
     1.7 -  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
     1.8 +  let val analz_impI = OldGoals.inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
     1.9    in
    1.10      rtac analz_impI THEN' 
    1.11      REPEAT1 o 
    1.12 @@ -299,7 +299,7 @@
    1.13  ML
    1.14  {*
    1.15  val synth_analz_mono_contra_tac = 
    1.16 -  let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
    1.17 +  let val syan_impI = OldGoals.inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
    1.18    in
    1.19      rtac syan_impI THEN' 
    1.20      REPEAT1 o