src/ZF/list.ML
changeset 124 858ab9a9b047
parent 84 01d6c0ddaae3
child 279 7738aed3f84d
--- 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*)