--- a/src/HOL/Record.thy Thu Aug 27 00:40:53 2009 +1000
+++ b/src/HOL/Record.thy Thu Sep 10 15:18:43 2009 +1000
@@ -7,7 +7,7 @@
theory Record
imports Product_Type IsTuple
-uses ("Tools/record_package.ML")
+uses ("Tools/record.ML")
begin
lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
@@ -65,7 +65,7 @@
"_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
"_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
-use "Tools/record_package.ML"
-setup RecordPackage.setup
+use "Tools/record.ML"
+setup Record.setup
end