diff -r 663cead79989 -r ad45e477926c List.ML
--- a/List.ML	Wed Dec 07 14:12:27 1994 +0100
+++ b/List.ML	Thu Dec 08 12:50:38 1994 +0100
@@ -10,11 +10,10 @@
 
 val [Nil_not_Cons,Cons_not_Nil] = list.distinct;
 
-val Cons_neq_Nil = store_thm("Cons_neq_Nil", standard (Cons_not_Nil RS notE));
-val Nil_neq_Cons = store_thm("Nil_neq_Cons", sym RS Cons_neq_Nil);
+bind_thm("Cons_neq_Nil", standard (Cons_not_Nil RS notE));
+bind_thm("Nil_neq_Cons", sym RS Cons_neq_Nil);
 
-val Cons_inject =
-  store_thm("Cons_inject", standard ((hd list.inject) RS iffD1 RS conjE));
+bind_thm("Cons_inject", standard ((hd list.inject) RS iffD1 RS conjE));
 
 val list_ss = HOL_ss addsimps list.simps;