--- a/src/HOL/Rational.thy Wed Jun 17 08:13:05 2009 +0200
+++ b/src/HOL/Rational.thy Wed Jun 17 08:21:27 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