src/HOL/Rat.thy

--- a/src/HOL/Rat.thy	Wed Apr 08 23:00:09 2015 +0200
+++ b/src/HOL/Rat.thy	Thu Apr 09 09:12:47 2015 +0200
@@ -610,8 +610,7 @@
 end
 
 lemma floor_Fract: "floor (Fract a b) = a div b"
-  using rat_floor_lemma [of a b]
-  by (simp add: floor_unique)
+  by (simp add: Fract_of_int_quotient floor_divide_of_int_eq)
 
 
 subsection {* Linear arithmetic setup *}