# HG changeset patch
# User haftmann
# Date 1361299450 -3600
# Node ID 9b5bf1a9a710b89d5585a315f4c6b9680f6b5808
# Parent  c344cf148e8ff023f038c6a9a8567e8949dc873d
dropped spurious left-over from 0a2371e7ced3

diff -r c344cf148e8f -r 9b5bf1a9a710 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Tue Feb 19 17:01:06 2013 +0100
+++ b/src/HOL/Library/Cardinality.thy	Tue Feb 19 19:44:10 2013 +0100
@@ -234,8 +234,6 @@
   dest!: finite_imageD intro: inj_onI)
 end
 
-declare [[show_consts]]
-
 instantiation integer :: card_UNIV begin
 definition "finite_UNIV = Phantom(integer) False"
 definition "card_UNIV = Phantom(integer) 0"