# HG changeset patch
# User paulson
# Date 927553707 -7200
# Node ID 1ca01fc3cca147313910cd36526162ba5009c81b
# Parent  62beb3336b02fdf46ebe37e8f24f9a69f2325fa3
expandshort

diff -r 62beb3336b02 -r 1ca01fc3cca1 src/HOL/UNITY/NSP_Bad.ML
--- a/src/HOL/UNITY/NSP_Bad.ML	Mon May 24 15:47:57 1999 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML	Mon May 24 15:48:27 1999 +0200
@@ -59,7 +59,7 @@
 
 fun ns_constrains_tac i = 
    SELECT_GOAL
-      (EVERY [REPEAT (eresolve_tac [Always_ConstrainsI] 1),
+      (EVERY [REPEAT (etac Always_ConstrainsI 1),
 	      REPEAT (resolve_tac [StableI, stableI,
 				   constrains_imp_Constrains] 1),
 	      rtac constrainsI 1,
@@ -90,7 +90,7 @@
 Addsimps [impOfAlways Spy_see_priK];
 
 Goal "Nprg : Always {s. (Key (priK A) : analz (spies s)) = (A : bad)}";
-br (Always_reachable RS Always_weaken) 1;
+by (rtac (Always_reachable RS Always_weaken) 1);
 by Auto_tac;
 qed "Spy_analz_priK";
 Addsimps [impOfAlways Spy_analz_priK];