--- 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;