# HG changeset patch
# User haftmann
# Date 1257865906 -3600
# Node ID 27c5023ee8182565170984c3ae0ab7ae0276b90b
# Parent  7264824baf660acec75c30ea9e3f67c866b32369
tuned header

diff -r 7264824baf66 -r 27c5023ee818 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Tue Nov 10 16:11:43 2009 +0100
+++ b/src/HOL/ex/Records.thy	Tue Nov 10 16:11:46 2009 +0100
@@ -5,7 +5,9 @@
 
 header {* Using extensible records in HOL -- points and coloured points *}
 
-theory Records imports Main begin
+theory Records
+imports Main Record
+begin
 
 subsection {* Points *}