--- a/Sum.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/Sum.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -40,7 +40,7 @@
 by (rtac Inr_RepI 1);
 qed "Inl_not_Inr";
 
-val Inl_neq_Inr = standard (Inl_not_Inr RS notE);
+bind_thm ("Inl_neq_Inr", (Inl_not_Inr RS notE));
 val Inr_neq_Inl = sym RS Inl_neq_Inr;
 
 goal Sum.thy "(Inl(a)=Inr(b)) = False";