tuned;

--- a/src/HOL/Record.thy	Thu Oct 18 21:07:29 2001 +0200
+++ b/src/HOL/Record.thy	Thu Oct 18 21:22:40 2001 +0200
@@ -13,7 +13,7 @@
 
 constdefs
   product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) =>
-    ('a => 'b => 'p) => ('p \<Rightarrow> 'a) => ('p => 'b) => bool"
+    ('a => 'b => 'p) => ('p => 'a) => ('p => 'b) => bool"
   "product_type Rep Abs pair dest1 dest2 ==
     type_definition Rep Abs UNIV \<and>
     pair = (\<lambda>a b. Abs (a, b)) \<and>
@@ -23,8 +23,8 @@
 lemma product_typeI:
   "type_definition Rep Abs UNIV ==>
     pair == \<lambda>a b. Abs (a, b) ==>
-    dest1 == (\<lambda>p. fst (Rep p)) \<Longrightarrow>
-    dest2 == (\<lambda>p. snd (Rep p)) \<Longrightarrow>
+    dest1 == (\<lambda>p. fst (Rep p)) ==>
+    dest2 == (\<lambda>p. snd (Rep p)) ==>
     product_type Rep Abs pair dest1 dest2"
   by (simp add: product_type_def)
 
@@ -93,10 +93,10 @@
 
 theorem product_type_cases [cases set: product_type]:
   "product_type Rep Abs pair dest1 dest2 ==>
-    (!!x y. p = pair x y \<Longrightarrow> C) ==> C"
+    (!!x y. p = pair x y ==> C) ==> C"
 proof -
   assume prod_type: "product_type Rep Abs pair dest1 dest2"
-  assume "!!x y. p = pair x y \<Longrightarrow> C"
+  assume "!!x y. p = pair x y ==> C"
   with prod_type show C
     by (induct p) (simp only: product_type_inject [OF prod_type], blast)
 qed
@@ -112,7 +112,7 @@
 
 theorem product_type_split_paired_all:
   "product_type Rep Abs pair dest1 dest2 ==>
-  (\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (pair a b))"
+  (!!x. PROP P x) == (!!a b. PROP P (pair a b))"
 proof
   fix a b
   assume "!!x. PROP P x"
@@ -126,19 +126,13 @@
 qed
 
 
-text {* \medskip Type class for record extensions. *}
+subsection {* Type class for record extensions *}
 
 axclass more < "term"
 instance unit :: more ..
 
 
-subsection {* Record package setup *}
-
-use "Tools/record_package.ML"
-setup RecordPackage.setup
-
-
-subsection {* Concrete syntax *}
+subsection {* Concrete record syntax *}
 
 nonterminals
   ident field_type field_types field fields update updates
@@ -172,17 +166,10 @@
   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
 
-parse_translation {*
-  let
-    fun update_name_tr (Free (x, T) :: ts) =
-          Term.list_comb (Free (suffix RecordPackage.updateN x, T), ts)
-      | update_name_tr (Const (x, T) :: ts) =
-          Term.list_comb (Const (suffix RecordPackage.updateN x, T), ts)
-      | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
-          Term.list_comb (c $ update_name_tr [t] $
-            (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
-      | update_name_tr ts = raise TERM ("update_name_tr", ts);
-  in [("_update_name", update_name_tr)] end
-*}
+
+subsection {* Package setup *}
+
+use "Tools/record_package.ML"
+setup RecordPackage.setup
 
 end

--- a/src/HOL/Tools/record_package.ML	Thu Oct 18 21:07:29 2001 +0200
+++ b/src/HOL/Tools/record_package.ML	Thu Oct 18 21:22:40 2001 +0200
@@ -50,8 +50,6 @@
 val product_type_inject = thm "product_type_inject";
 val product_type_conv1 = thm "product_type_conv1";
 val product_type_conv2 = thm "product_type_conv2";
-val product_type_induct = thm "product_type_induct";
-val product_type_cases = thm "product_type_cases";
 val product_type_split_paired_all = thm "product_type_split_paired_all";
 
 
@@ -113,13 +111,6 @@
 val AbsN = "Abs_";
 
 
-(** generic operations **)
-
-(* adhoc priming of vars *)
-
-fun prime (Free (x, T)) = Free (x ^ "'", T)
-  | prime t = raise TERM ("prime: no free variable", [t]);
-
 
 (** tuple operations **)
 
@@ -148,7 +139,7 @@
 fun mk_Abs U (c, T) =
   Const (suffix field_typeN (prefix_base AbsN c),
     HOLogic.mk_prodT (T, U) --> mk_fieldT ((c, T), U));
-  
+
 
 (* constructors *)
 
@@ -266,12 +257,21 @@
   | record_update_tr ts = raise TERM ("record_update_tr", ts);
 
 
+fun update_name_tr (Free (x, T) :: ts) = Term.list_comb (Free (suffix updateN x, T), ts)
+  | update_name_tr (Const (x, T) :: ts) = Term.list_comb (Const (suffix updateN x, T), ts)
+  | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
+      Term.list_comb (c $ update_name_tr [t] $
+        (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
+  | update_name_tr ts = raise TERM ("update_name_tr", ts);
+
+
 val parse_translation =
  [("_record_type", record_type_tr),
   ("_record_type_scheme", record_type_scheme_tr),
   ("_record", record_tr),
   ("_record_scheme", record_scheme_tr),
-  ("_record_update", record_update_tr)];
+  ("_record_update", record_update_tr),
+  ("_update_name", update_name_tr)];
 
 
 (* print translations *)