src/HOL/Auth/OtwayRees_Bad.ML

--- a/src/HOL/Auth/OtwayRees_Bad.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -125,7 +125,7 @@
       (!claset addIs [impOfSubs analz_subset_parts]
                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
-               addss (!simpset)) 1);
+               unsafe_addss (!simpset)) 1);
 (*OR1-3*)
 by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
 qed_spec_mp "new_keys_not_used";