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