src/Pure/ROOT.ML
changeset 59470 31d810570879
parent 59363 4660b0409096
child 59714 ae322325adbb
     1.1 --- a/src/Pure/ROOT.ML	Thu Jan 29 15:27:29 2015 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Jan 29 16:16:01 2015 +0100
     1.3 @@ -94,12 +94,6 @@
     1.4  then use "ML/exn_properties_polyml.ML"
     1.5  else use "ML/exn_properties_dummy.ML";
     1.6  
     1.7 -if ML_System.name = "polyml-5.5.1"
     1.8 -  orelse ML_System.name = "polyml-5.5.2"
     1.9 -  orelse ML_System.name = "polyml-5.5.3"
    1.10 -then use "ML/exn_trace_polyml-5.5.1.ML"
    1.11 -else ();
    1.12 -
    1.13  if ML_System.name = "polyml-5.5.0"
    1.14    orelse ML_System.name = "polyml-5.5.1"
    1.15    orelse ML_System.name = "polyml-5.5.2"