# HG changeset patch
# User haftmann
# Date 1245222508 -7200
# Node ID d0115c3038462ea45fbffbe9366791c0f6948f7e
# Parent  6cc4c63cc9904207ec74687e0207c1aa260d94f9
obey SML syntax even more closely

diff -r 6cc4c63cc990 -r d0115c303846 src/HOL/Rational.thy
--- 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