# HG changeset patch
# User wenzelm
# Date 1213200936 -7200
# Node ID 9506c7e73cfae0674dc4d191d29c710108bc6cf4
# Parent  113a32dd0b14fe33678242289d35e36fef57d6a1
OldGoals.inst;

diff -r 113a32dd0b14 -r 9506c7e73cfa src/HOL/SET-Protocol/EventSET.thy
--- a/src/HOL/SET-Protocol/EventSET.thy	Wed Jun 11 18:04:02 2008 +0200
+++ b/src/HOL/SET-Protocol/EventSET.thy	Wed Jun 11 18:15:36 2008 +0200
@@ -180,7 +180,7 @@
 ML
 {*
 val analz_mono_contra_tac = 
-  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
+  let val analz_impI = OldGoals.inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
   in rtac analz_impI THEN' 
      REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) THEN'
      mp_tac
diff -r 113a32dd0b14 -r 9506c7e73cfa src/HOL/SET-Protocol/MessageSET.thy
--- a/src/HOL/SET-Protocol/MessageSET.thy	Wed Jun 11 18:04:02 2008 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Wed Jun 11 18:15:36 2008 +0200
@@ -815,7 +815,7 @@
     be pulled out using the @{text analz_insert} rules*}
 ML
 {*
-fun insComm x y = inst "x" x (inst "y" y insert_commute);
+fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
 
 bind_thms ("pushKeys",
            map (insComm "Key ?K")