src/HOL/Quotient_Examples/Quotient_Rat.thy

--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Wed May 30 18:09:23 2012 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Thu May 31 10:01:15 2012 +0200
@@ -114,6 +114,8 @@
 
 lemmas [simp] = Respects_def
 
+(* FIXME: (partiality_)descending raises exception TYPE_MATCH
+
 instantiation rat :: comm_ring_1
 begin
 
@@ -260,5 +262,6 @@
     then show "\<exists>z\<Colon>int. a * b \<le> z * b * b" by auto
   qed
 qed
+*)
 
 end