src/Pure/ML-Systems/polyml.ML

 
 fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
 
 if ML_System.name = "polyml-5.5.1"
   orelse ML_System.name = "polyml-5.5.2"
-  orelse ML_System.name = "polyml-5.5.3"
   orelse ML_System.name = "polyml-5.6"
 then use "ML-Systems/exn_trace_polyml-5.5.1.ML"
 else ();
 
 

 
 open Thread;
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/multithreading_polyml.ML";
 
-if ML_System.name = "polyml-5.5.3"
-  orelse ML_System.name = "polyml-5.6"
-then use "ML-Systems/ml_stack_polyml-5.5.3.ML"
+if ML_System.name = "polyml-5.6"
+then use "ML-Systems/ml_stack_polyml-5.6.ML"
 else use "ML-Systems/ml_stack_dummy.ML";
 
 use "ML-Systems/unsynchronized.ML";
 val _ = PolyML.Compiler.forgetValue "ref";
 val _ = PolyML.Compiler.forgetType "ref";

   open ML_Name_Space;
   val display_val = pretty_ml o displayVal;
 end;
 
 use "ML-Systems/ml_compiler_parameters.ML";
-if ML_System.name = "polyml-5.5.3"
-  orelse ML_System.name = "polyml-5.6"
-then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
+if ML_System.name = "polyml-5.6"
+then use "ML-Systems/ml_compiler_parameters_polyml-5.6.ML" else ();
 
 use "ML-Systems/use_context.ML";
 use "ML-Systems/ml_positions.ML";
 use "ML-Systems/compiler_polyml.ML";
 

 PolyML.Compiler.maxInlineSize := 80;
 
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
 
 use "ML-Systems/ml_parse_tree.ML";
-if ML_System.name = "polyml-5.5.3"
-  orelse ML_System.name = "polyml-5.6"
-then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
+if ML_System.name = "polyml-5.6"
+then use "ML-Systems/ml_parse_tree_polyml-5.6.ML" else ();
 
 fun toplevel_pp context (_: string list) pp =
   use_text context {line = 1, file = "pp", verbose = false, debug = false}
     ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
 

     struct_name ^ ".ML_print_depth ())))))";
 
 
 (* ML debugger *)
 
-if ML_System.name = "polyml-5.5.3"
-  orelse ML_System.name = "polyml-5.6"
-then use "ML-Systems/ml_debugger_polyml-5.5.3.ML"
+if ML_System.name = "polyml-5.6"
+then use "ML-Systems/ml_debugger_polyml-5.6.ML"
 else use "ML-Systems/ml_debugger.ML";