# HG changeset patch
# User haftmann
# Date 1245219687 -7200
# Node ID 2f8e3150e07316ed57a922ef00e96ad34dd12735
# Parent  81e5e8ffe92fb873e9de8f53ba160f9874c6b33f
obey SML syntax more closely

diff -r 81e5e8ffe92f -r 2f8e3150e073 src/HOL/Rational.thy
--- 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