# HG changeset patch
# User wenzelm
# Date 1027462284 -7200
# Node ID 0b60b9e18a26fa9d0aa984ff6ba6f0052d9fc0be
# Parent  666137b488a4728d06050f460eca06940a024eb6
adapted fact names;

diff -r 666137b488a4 -r 0b60b9e18a26 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Jul 24 00:10:52 2002 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed Jul 24 00:11:24 2002 +0200
@@ -46,12 +46,12 @@
 val product_typeN = "Record.product_type";
 
 val product_typeI = thm "product_typeI";
-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";
+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";
 
 
 
diff -r 666137b488a4 -r 0b60b9e18a26 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Wed Jul 24 00:10:52 2002 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Wed Jul 24 00:11:24 2002 +0200
@@ -35,17 +35,16 @@
 (** theory context references **)
 
 val type_definitionN = "Typedef.type_definition";
-val type_definition_def = thm "type_definition_def";
 
-val Rep = thm "Rep";
-val Rep_inverse = thm "Rep_inverse";
-val Abs_inverse = thm "Abs_inverse";
-val Rep_inject = thm "Rep_inject";
-val Abs_inject = thm "Abs_inject";
-val Rep_cases = thm "Rep_cases";
-val Abs_cases = thm "Abs_cases";
-val Rep_induct = thm "Rep_induct";
-val Abs_induct = thm "Abs_induct";
+val Rep = thm "type_definition.Rep";
+val Rep_inverse = thm "type_definition.Rep_inverse";
+val Abs_inverse = thm "type_definition.Abs_inverse";
+val Rep_inject = thm "type_definition.Rep_inject";
+val Abs_inject = thm "type_definition.Abs_inject";
+val Rep_cases = thm "type_definition.Rep_cases";
+val Abs_cases = thm "type_definition.Abs_cases";
+val Rep_induct = thm "type_definition.Rep_induct";
+val Abs_induct = thm "type_definition.Abs_induct";