--- 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"