diff -r 4d0545e93c0d -r c533bc92e882 HOL.ML
--- a/HOL.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/HOL.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -16,7 +16,7 @@
  (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
 
 (*calling "standard" reduces maxidx to 0*)
-val ssubst = standard (sym RS subst);
+bind_thm ("ssubst", (sym RS subst));
 
 qed_goal "trans" HOL.thy "[| r=s; s=t |] ==> r=t"
  (fn prems =>