diff -r 5a6f2aabd538 -r 6bcb44e4d6e5 src/ZF/Datatype.ML
--- a/src/ZF/Datatype.ML	Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/Datatype.ML	Tue Jan 30 13:42:57 1996 +0100
@@ -26,9 +26,9 @@
 
 signature INDUCTIVE_THMS =
   sig
-  val monos      : thm list		(*monotonicity of each M operator*)
-  val type_intrs : thm list		(*type-checking intro rules*)
-  val type_elims : thm list		(*type-checking elim rules*)
+  val monos      : thm list             (*monotonicity of each M operator*)
+  val type_intrs : thm list             (*type-checking intro rules*)
+  val type_elims : thm list             (*type-checking elim rules*)
   end;
 
 functor Data_section_Fun
@@ -37,7 +37,7 @@
 struct
 
 structure Con = Constructor_Fun 
- 	(structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
+        (structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
 
 structure Inductive = Ind_section_Fun
    (open Arg; 
@@ -55,7 +55,7 @@
 struct
 
 structure Con = Constructor_Fun 
- 	(structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
+        (structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
 
 structure CoInductive = CoInd_section_Fun
    (open Arg;