# HG changeset patch
# User wenzelm
# Date 972292440 -7200
# Node ID 475ea668c67d148580f456f7909755ed8f56ba8c
# Parent  00abecbfa46afec0927ac43503787c40566e36d5
tuned deps;

diff -r 00abecbfa46a -r 475ea668c67d src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Oct 23 10:20:55 2000 +0200
+++ b/src/HOL/Product_Type.thy	Mon Oct 23 11:14:00 2000 +0200
@@ -7,7 +7,7 @@
 The unit type.
 *)
 
-Product_Type = Fun + equalities +
+Product_Type = Fun +
 
 
 (** products **)