diff -r 313d3b697c9a -r a8758f47f9e8 src/Pure/ML/fixed_int_dummy.ML
--- a/src/Pure/ML/fixed_int_dummy.ML	Mon Apr 04 16:52:56 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(*  Title:      Pure/ML/fixed_int_dummy.ML
-
-FixedInt dummy that is not fixed (up to Poly/ML 5.6).
-*)
-
-structure FixedInt = IntInf;