src/HOL/Record.thy

--- a/src/HOL/Record.thy	Wed Jul 24 22:14:42 2002 +0200
+++ b/src/HOL/Record.thy	Wed Jul 24 22:15:55 2002 +0200
@@ -18,9 +18,6 @@
     and dest1: "dest1 == (\<lambda>p. fst (Rep p))"
     and dest2: "dest2 == (\<lambda>p. snd (Rep p))"
 
-lemmas product_typeI =
-  product_type.intro [OF product_type_axioms.intro]
-
 lemma (in product_type)
     "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
   by (simp add: pair type_definition.Abs_inject [OF "typedef"])