--- a/src/Pure/ML-Systems/proper_int.ML Sun Mar 20 22:47:08 2011 +0100
+++ b/src/Pure/ML-Systems/proper_int.ML Sun Mar 20 22:48:08 2011 +0100
@@ -13,8 +13,6 @@
(* Int *)
-structure OrigInt = Int;
-structure OrigIntInf = IntInf;
type int = IntInf.int;
structure IntInf =