diff -r 5844017e31f8 -r 7fa17a225852 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sun Apr 11 16:51:06 2010 +0200
+++ b/src/HOL/Rat.thy	Sun Apr 11 16:51:07 2010 +0200
@@ -1019,11 +1019,9 @@
 definition Frct :: "int \<times> int \<Rightarrow> rat" where
   [simp]: "Frct p = Fract (fst p) (snd p)"
 
-code_abstype Frct quotient_of
-proof (rule eq_reflection)
-  fix r :: rat
-  show "Frct (quotient_of r) = r" by (cases r) (auto intro: quotient_of_eq)
-qed
+lemma [code abstype]:
+  "Frct (quotient_of q) = q"
+  by (cases q) (auto intro: quotient_of_eq)
 
 lemma Frct_code_post [code_post]:
   "Frct (0, k) = 0"