src/HOL/Rat.thy

--- a/src/HOL/Rat.thy	Fri Feb 26 09:20:18 2010 +0100
+++ b/src/HOL/Rat.thy	Fri Feb 26 10:48:20 2010 +0100
@@ -1168,6 +1168,9 @@
   Fract ("(_,/ _)")
 
 consts_code
+  quotient_of ("{*normalize*}")
+
+consts_code
   "of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int")
 attach {*
 fun rat_of_int i = (i, 1);