# HG changeset patch
# User Andreas Lochbihler
# Date 1338551571 -7200
# Node ID 11a732f7d79f7938f31e37608f52554185092ddf
# Parent  60bcc6cf17d6cacc73f3662b2c3e9879c680a0a5
drop redundant sort constraint

diff -r 60bcc6cf17d6 -r 11a732f7d79f src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Fri Jun 01 08:32:26 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Fri Jun 01 13:52:51 2012 +0200
@@ -44,7 +44,7 @@
 lemma card_unit [simp]: "CARD(unit) = 1"
   unfolding UNIV_unit by simp
 
-lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a::finite) * CARD('b::finite)"
+lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a) * CARD('b)"
   unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
 
 lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)"