diff -r 4d0545e93c0d -r c533bc92e882 List.ML
--- a/List.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/List.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -10,10 +10,10 @@
 
 val [Nil_not_Cons,Cons_not_Nil] = list.distinct;
 
-bind_thm("Cons_neq_Nil", standard (Cons_not_Nil RS notE));
+bind_thm("Cons_neq_Nil", Cons_not_Nil RS notE);
 bind_thm("Nil_neq_Cons", sym RS Cons_neq_Nil);
 
-bind_thm("Cons_inject", standard ((hd list.inject) RS iffD1 RS conjE));
+bind_thm("Cons_inject", (hd list.inject) RS iffD1 RS conjE);
 
 val list_ss = HOL_ss addsimps list.simps;