--- a/src/HOL/Auth/Yahalom2.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Sat Feb 15 17:52:31 1997 +0100
@@ -17,6 +17,7 @@
proof_timing:=true;
HOL_quantifiers := false;
+val op addss = op unsafe_addss;
(*A "possibility property": there are traces that reach the end*)
goal thy