--- 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);