src/ZF/fin.ML

--- a/src/ZF/fin.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/fin.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -18,13 +18,12 @@
 *)
 
 structure Fin = Inductive_Fun
- (val thy = Arith.thy addconsts [(["Fin"],"i=>i")];
-  val rec_doms = [("Fin","Pow(A)")];
-  val sintrs = 
-	  ["0 : Fin(A)",
-	   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"];
-  val monos = [];
-  val con_defs = [];
+ (val thy        = Arith.thy addconsts [(["Fin"],"i=>i")]
+  val rec_doms   = [("Fin","Pow(A)")]
+  val sintrs     = ["0 : Fin(A)",
+                    "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"]
+  val monos      = []
+  val con_defs   = []
   val type_intrs = [empty_subsetI, cons_subsetI, PowI]
   val type_elims = [make_elim PowD]);