diff -r d8cf59edf819 -r 82859dac5f59 src/Pure/ROOT --- a/src/Pure/ROOT Mon Apr 04 20:45:54 2016 +0200 +++ b/src/Pure/ROOT Mon Apr 04 20:46:39 2016 +0200 @@ -98,7 +98,6 @@ "Isar/typedecl.ML" "ML/exn_debugger.ML" "ML/exn_properties.ML" - "ML/fixed_int_dummy.ML" "ML/ml_antiquotation.ML" "ML/ml_antiquotations.ML" "ML/ml_compiler.ML"