src/ZF/List.ML

--- a/src/ZF/List.ML	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/List.ML	Tue Nov 16 14:24:21 1993 +0100
@@ -21,6 +21,8 @@
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);
 
+store_theory "List" List.thy;
+
 val [NilI, ConsI] = List.intrs;
 
 (*An elimination rule, for type-checking*)