--- a/src/ZF/List.ML Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/List.ML Thu May 23 17:05:21 2002 +0200
@@ -8,6 +8,8 @@
(*** Aspects of the datatype definition ***)
+Addsimps list.intrs;
+
(*An elimination rule, for type-checking*)
bind_thm ("ConsE", list.mk_cases "Cons(a,l) : list(A)");