tuned;

--- a/src/HOL/HOL_lemmas.ML	Sat Oct 27 23:19:55 2001 +0200
+++ b/src/HOL/HOL_lemmas.ML	Sat Oct 27 23:21:19 2001 +0200
@@ -6,7 +6,7 @@
 Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68.
 *)
 
-(* ML bindings *)
+(* legacy ML bindings *)
 
 val plusI = thm "plusI";
 val minusI = thm "minusI";