--- a/src/HOL/Rational.thy Wed Jun 17 08:31:13 2009 +0200
+++ b/src/HOL/Rational.thy Wed Jun 17 09:08:28 2009 +0200
@@ -1060,7 +1060,7 @@
consts_code
"of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int")
attach {*
-fun = rat_of_int i (i, 1);
+fun rat_of_int i = (i, 1);
*}
end