src/ZF/List.ML

--- a/src/ZF/List.ML	Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/List.ML	Fri Jul 15 13:34:31 1994 +0200
@@ -8,6 +8,7 @@
 
 structure List = Datatype_Fun
  (val thy        = Univ.thy
+  val thy_name   = "List"
   val rec_specs  = [("list", "univ(A)",
                       [(["Nil"],    "i", NoSyn), 
                        (["Cons"],   "[i,i]=>i", NoSyn)])]
@@ -18,8 +19,6 @@
   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*)