diff -r da15d528fb19 -r f4f9946ad741 List.ML
--- a/List.ML	Thu Nov 25 10:04:02 1993 +0100
+++ b/List.ML	Mon Nov 29 18:35:02 1993 +0100
@@ -374,3 +374,12 @@
 by(ALLGOALS(asm_simp_tac(map_ss addsimps
        [Rep_map_type,List_Sexp RS subsetD])));
 val Abs_Rep_map = result();
+
+val list_ss = arith_ss addsimps
+  [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq,
+   list_rec_Nil, list_rec_Cons,
+   null_Nil, null_Cons, hd_Cons, tl_Cons,
+   list_case_Nil, list_case_Cons,
+   append_Nil, append_Cons, append_assoc,
+   map_Nil, map_Cons, map_ident,
+   list_all_Nil, list_all_Cons];