src/ZF/ex/tf.ML

--- a/src/ZF/ex/tf.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/tf.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -7,20 +7,19 @@
 *)
 
 structure TF = Datatype_Fun
- (val thy = Univ.thy;
-  val rec_specs = 
-      [("tree", "univ(A)",
-	  [(["Tcons"],	"[i,i]=>i")]),
-       ("forest", "univ(A)",
-	  [(["Fnil"],	"i"),
-	   (["Fcons"],	"[i,i]=>i")])];
-  val rec_styp = "i=>i";
-  val ext = None
-  val sintrs = 
-	  ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
-	   "Fnil : forest(A)",
-	   "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"];
-  val monos = [];
+ (val thy        = Univ.thy
+  val rec_specs  = [("tree", "univ(A)",
+                       [(["Tcons"],  "[i,i]=>i")]),
+                    ("forest", "univ(A)",
+                       [(["Fnil"],   "i"),
+                        (["Fcons"],  "[i,i]=>i")])]
+  val rec_styp   = "i=>i"
+  val ext        = None
+  val sintrs     = 
+          ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
+           "Fnil : forest(A)",
+           "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"]
+  val monos      = []
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);