diff -r a97e9caebd60 -r c4e9a48bc50e src/HOL/Record.thy
--- a/src/HOL/Record.thy	Sat Aug 15 15:29:54 2009 +0200
+++ b/src/HOL/Record.thy	Thu Aug 27 00:40:53 2009 +1000
@@ -1,26 +1,36 @@
 (*  Title:      HOL/Record.thy
+    ID:         $Id: Record.thy,v 1.33 2007/12/19 15:32:12 schirmer Exp $
     Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
 *)
 
 header {* Extensible records with structural subtyping *}
 
 theory Record
-imports Product_Type
-uses ("Tools/record.ML")
+imports Product_Type IsTuple
+uses ("Tools/record_package.ML")
 begin
 
 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
   by simp
 
-lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
-  by simp
-
-lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
-  by simp
-
 lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" 
   by (simp add: comp_def)
 
+lemma meta_iffD2:
+  "\<lbrakk> PROP P \<equiv> PROP Q; PROP Q \<rbrakk> \<Longrightarrow> PROP P"
+  by simp
+
+lemma o_eq_dest_lhs:
+  "a o b = c \<Longrightarrow> a (b v) = c v"
+  by clarsimp
+
+lemma id_o_refl:
+  "id o f = f o id"
+  by simp
+
+lemma o_eq_id_dest:
+  "a o b = id o c \<Longrightarrow> a (b v) = c v"
+  by clarsimp
 
 subsection {* Concrete record syntax *}
 
@@ -55,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.ML"
-setup Record.setup
+use "Tools/record_package.ML"
+setup RecordPackage.setup
 
 end