src/ZF/List.ML

--- a/src/ZF/List.ML	Wed Jun 29 12:13:03 1994 +0200
+++ b/src/ZF/List.ML	Fri Jul 01 11:03:42 1994 +0200
@@ -9,10 +9,9 @@
 structure List = Datatype_Fun
  (val thy        = Univ.thy
   val rec_specs  = [("list", "univ(A)",
-                      [(["Nil"],    "i"), 
-                       (["Cons"],   "[i,i]=>i")])]
+                      [(["Nil"],    "i", NoSyn), 
+                       (["Cons"],   "[i,i]=>i", NoSyn)])]
   val rec_styp   = "i=>i"
-  val ext        = None
   val sintrs     = ["Nil : list(A)",
                     "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"]
   val monos      = []