eliminated duplicate;
authorwenzelm
Sat Mar 26 12:17:02 2016 +0100 (2016-03-26)
changeset 62710e17f014775a0
parent 62709 fe3d50448833
child 62711 09df6a51ad3c
eliminated duplicate;
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ROOT.ML	Sat Mar 26 12:12:13 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Sat Mar 26 12:17:02 2016 +0100
     1.3 @@ -250,7 +250,6 @@
     1.4  use "ML/ml_env.ML";
     1.5  use "ML/ml_options.ML";
     1.6  use_no_debug "ML/exn_debugger.ML";
     1.7 -use "ML/ml_options.ML";
     1.8  use_no_debug "Isar/runtime.ML";
     1.9  use "PIDE/execution.ML";
    1.10  use "ML/ml_compiler.ML";