# HG changeset patch
# User wenzelm
# Date 884770344 -3600
# Node ID fe504f608835eecab5fbad406244d313e4785274
# Parent  a259399ac328e575c4aa247e20a3c4afb3f9134d
added record.ML;

diff -r a259399ac328 -r fe504f608835 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Jan 14 10:31:32 1998 +0100
+++ b/src/HOL/ROOT.ML	Wed Jan 14 10:32:24 1998 +0100
@@ -39,6 +39,8 @@
 use_thy "Sum";
 use_thy "Gfp";
 
+use "record.ML";
+
 use "datatype.ML";
 use_thy "Arith";
 use "arith_data.ML";