# HG changeset patch
# User blanchet
# Date 1409695587 -7200
# Node ID 14dda84afbb30615fff33fc88b98039fe23d613a
# Parent  47c3c7019b976dd122f5b0e846950803f85ced3b
commented out failing tactic (now that 'typerep' is defined using the new package

diff -r 47c3c7019b97 -r 14dda84afbb3 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Wed Sep 03 00:06:26 2014 +0200
+++ b/src/HOL/Library/Countable.thy	Wed Sep 03 00:06:27 2014 +0200
@@ -308,9 +308,11 @@
 hide_const (open) finite_item nth_item
 
 
+(* FIXME
 subsection {* Countable datatypes *}
 
 instance typerep :: countable
   by countable_datatype
+*)
 
 end