--- a/src/HOL/UNITY/Simple/NSP_Bad.ML Thu Jan 30 10:35:56 2003 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.ML Thu Jan 30 18:08:09 2003 +0100
@@ -31,10 +31,10 @@
Goal "A ~= B ==> EX NB. EX s: reachable Nprg. \
\ Says A B (Crypt (pubK B) (Nonce NB)) : set s";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (res_inst_tac [("act", "NS3")] reachable.Acts 2);
-by (res_inst_tac [("act", "NS2")] reachable.Acts 3);
-by (res_inst_tac [("act", "NS1")] reachable.Acts 4);
-by (rtac reachable.Init 5);
+by (res_inst_tac [("act", "NS3")] reachable_Acts 2);
+by (res_inst_tac [("act", "NS2")] reachable_Acts 3);
+by (res_inst_tac [("act", "NS1")] reachable_Acts 4);
+by (rtac reachable_Init 5);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def])));
by (REPEAT_FIRST (rtac exI ));
by possibility_tac;