src/ZF/list.ML
changeset 279 7738aed3f84d
parent 124 858ab9a9b047
--- a/src/ZF/list.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/list.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -7,17 +7,15 @@
 *)
 
 structure List = Datatype_Fun
- (val thy = Univ.thy;
-  val rec_specs = 
-      [("list", "univ(A)",
-	  [(["Nil"],	"i"), 
-	   (["Cons"],	"[i,i]=>i")])];
-  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 = [];
+ (val thy        = Univ.thy
+  val rec_specs  = [("list", "univ(A)",
+                      [(["Nil"],    "i"), 
+                       (["Cons"],   "[i,i]=>i")])]
+  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      = []
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);