--- a/src/Pure/RAW/fixed_int_dummy.ML Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(* Title: Pure/RAW/fixed_int_dummy.ML
-
-FixedInt dummy that is not fixed (up to Poly/ML 5.6).
-*)
-
-structure FixedInt = IntInf;