src/HOL/Auth/ROOT.ML

--- a/src/HOL/Auth/ROOT.ML	Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/ROOT.ML	Wed May 07 13:01:43 1997 +0200
@@ -12,6 +12,9 @@
 proof_timing := true;
 goals_limit := 1;
 
+(*New version of addss isn't ready--too slow*)
+val op addss = op unsafe_addss;
+
 (*Shared-key protocols*)
 time_use_thy "NS_Shared";
 time_use_thy "OtwayRees";