diff -r f7d54060b5b0 -r 93d1ad7662a9 src/Tools/integer.ML
--- a/src/Tools/integer.ML	Thu Jun 28 19:09:41 2007 +0200
+++ b/src/Tools/integer.ML	Thu Jun 28 19:09:43 2007 +0200
@@ -43,6 +43,8 @@
 
 open IntInf;
 
+type integer = int;
+
 val int = fromInt;
 
 val zero = int 0;
@@ -110,6 +112,3 @@
 fun a >% b = b <% a;
 fun a >=% b = b <=% a;
 fun a <>% b = not (a =% b);
-
-val gcd = uncurry Integer.gcd; (*FIXME*)
-val lcm = uncurry Integer.lcm; (*FIXME*)