--- a/src/HOL/W0/I.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/W0/I.ML Sat Feb 15 17:52:31 1997 +0100
@@ -8,6 +8,8 @@
open I;
+val op addss = op unsafe_addss;
+
goal thy
"! a m s s' t n. \
\ (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) --> \