--- 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;