# HG changeset patch
# User lcp
# Date 775755297 -7200
# Node ID 15375d7b379c52015a9d9d86a0f15df2f8e49a3f
# Parent  77e36960fd9e5cf2bf416c9cf04d05ec6ec39a59
trivial whitespace change

diff -r 77e36960fd9e -r 15375d7b379c src/ZF/ex/Data.ML
--- a/src/ZF/ex/Data.ML	Mon Aug 01 17:24:46 1994 +0200
+++ b/src/ZF/ex/Data.ML	Mon Aug 01 17:34:57 1994 +0200
@@ -9,7 +9,7 @@
 
 structure Data = Datatype_Fun
  (val thy        = Univ.thy
-  val thy_name = "Data"
+  val thy_name 	 = "Data"
   val rec_specs  = [("data", "univ(A Un B)",
                        [(["Con0"],   "i",	    NoSyn),
                         (["Con1"],   "i=>i",	    NoSyn),