src/ZF/List.ML
changeset 6153 bff90585cce5
parent 6141 a6922171b396
child 9491 1a36151ee2fc
--- a/src/ZF/List.ML	Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/List.ML	Wed Jan 27 10:31:31 1999 +0100
@@ -166,9 +166,7 @@
     [list_rec_type, map_type, map_type2, app_type, length_type, 
      rev_type, flat_type, list_add_type];
 
-Addsimps list_typechecks;
-
-simpset_ref() := simpset() setSolver (type_auto_tac list_typechecks);
+AddTCs list_typechecks;
 
 
 (*** theorems about map ***)