# HG changeset patch
# User wenzelm
# Date 1027541582 -7200
# Node ID 902ec83c1ca913401fd81a5f3c008e3c80bb6706
# Parent  7c0ba9dba978a2809cc138fe9bee715f2d6c2fdb
tuned;

diff -r 7c0ba9dba978 -r 902ec83c1ca9 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Jul 24 17:59:12 2002 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed Jul 24 22:13:02 2002 +0200
@@ -45,7 +45,7 @@
 
 val product_typeN = "Record.product_type";
 
-val product_typeI = thm "product_typeI";
+val product_type_intro = thm "product_type.intro";
 val product_type_inject = thm "product_type.inject";
 val product_type_conv1 = thm "product_type.conv1";
 val product_type_conv2 = thm "product_type.conv2";
@@ -621,7 +621,7 @@
       |>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs1
       |>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs2;
 
-    val prod_types = map (fn (((a, b), c), d) => product_typeI OF [a, b, c, d])
+    val prod_types = map (fn (((a, b), c), d) => product_type_intro OF [a, b, c, d])
       (typedefs ~~ field_defs ~~ dest_defs1 ~~ dest_defs2);
 
 
diff -r 7c0ba9dba978 -r 902ec83c1ca9 src/HOL/ex/Locales.thy
--- a/src/HOL/ex/Locales.thy	Wed Jul 24 17:59:12 2002 +0200
+++ b/src/HOL/ex/Locales.thy	Wed Jul 24 22:13:02 2002 +0200
@@ -233,7 +233,11 @@
   exhibited directly as context parameters; logically this corresponds
   to a curried predicate definition:
 
-  @{thm [display] group_context_axioms_def [no_vars]}
+  @{thm [display] group_context_def [no_vars]}
+
+  The corresponding introduction rule is as follows:
+
+  @{thm [display] group_context.intro [no_vars]}
 
   Occasionally, this ``externalized'' version of the informal idea of
   classes of tuple structures may cause some inconveniences,