src/HOL/Record.thy
changeset 16417 9bc16273c2d4
parent 16114 8d453f906e43
child 17957 d31acb64aa9a
--- a/src/HOL/Record.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Record.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
 
 theory Record
 imports Product_Type
-files ("Tools/record_package.ML")
+uses ("Tools/record_package.ML")
 begin
 
 ML {*