# HG changeset patch
# User wenzelm
# Date 884770292 -3600
# Node ID a259399ac328e575c4aa247e20a3c4afb3f9134d
# Parent  6b02fc8a97f689ed6a89e5db7768209011f5ae2e
tuned;

diff -r 6b02fc8a97f6 -r a259399ac328 src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Wed Jan 14 10:30:44 1998 +0100
+++ b/src/HOL/thy_data.ML	Wed Jan 14 10:31:32 1998 +0100
@@ -7,9 +7,9 @@
 
 (*for records*)
 type record_info =
- {args:     (string * sort) list,
-  parent:   (typ list * string) option,
-  fields:   (string * typ) list}
+ {args: (string * sort) list,
+  parent: (typ list * string) option,
+  fields: (string * typ) list}
 
 (*for datatypes*)
 type datatype_info =