1.1 --- a/src/HOL/SET-Protocol/EventSET.thy	Wed Jun 11 18:04:02 2008 +0200
     1.2 +++ b/src/HOL/SET-Protocol/EventSET.thy	Wed Jun 11 18:15:36 2008 +0200
     1.3 @@ -180,7 +180,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 rtac analz_impI THEN' 
    1.10       REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) THEN'
    1.11       mp_tac

     2.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Wed Jun 11 18:04:02 2008 +0200
     2.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Wed Jun 11 18:15:36 2008 +0200
     2.3 @@ -815,7 +815,7 @@
     2.4      be pulled out using the @{text analz_insert} rules*}
     2.5  ML
     2.6  {*
     2.7 -fun insComm x y = inst "x" x (inst "y" y insert_commute);
     2.8 +fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
     2.9  
    2.10  bind_thms ("pushKeys",
    2.11             map (insComm "Key ?K")