--- a/src/Pure/IsaMakefile Wed Aug 11 12:50:33 2010 +0200
+++ b/src/Pure/IsaMakefile Wed Aug 11 13:39:36 2010 +0200
@@ -19,19 +19,33 @@
## Pure
-BOOTSTRAP_FILES = ML-Systems/bash.ML ML-Systems/compiler_polyml-5.0.ML \
- ML-Systems/compiler_polyml-5.2.ML ML-Systems/compiler_polyml-5.3.ML \
- ML-Systems/ml_name_space.ML ML-Systems/ml_pretty.ML \
- ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \
- ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \
- ML-Systems/polyml-5.1.ML ML-Systems/polyml-5.2.ML \
- ML-Systems/polyml-5.2.1.ML ML-Systems/polyml.ML \
- ML-Systems/polyml_common.ML ML-Systems/pp_polyml.ML \
- ML-Systems/proper_int.ML ML-Systems/single_assignment.ML \
- ML-Systems/single_assignment_polyml.ML ML-Systems/smlnj.ML \
- ML-Systems/thread_dummy.ML ML-Systems/timing.ML \
- ML-Systems/time_limit.ML ML-Systems/universal.ML \
- ML-Systems/unsynchronized.ML
+BOOTSTRAP_FILES = \
+ ML-Systems/bash.ML \
+ ML-Systems/compiler_polyml-5.0.ML \
+ ML-Systems/compiler_polyml-5.2.ML \
+ ML-Systems/compiler_polyml-5.3.ML \
+ ML-Systems/ml_name_space.ML \
+ ML-Systems/ml_pretty.ML \
+ ML-Systems/multithreading.ML \
+ ML-Systems/multithreading_polyml.ML \
+ ML-Systems/overloading_smlnj.ML \
+ ML-Systems/polyml-5.0.ML \
+ ML-Systems/polyml-5.1.ML \
+ ML-Systems/polyml-5.2.1.ML \
+ ML-Systems/polyml-5.2.ML \
+ ML-Systems/polyml.ML \
+ ML-Systems/polyml_common.ML \
+ ML-Systems/pp_polyml.ML \
+ ML-Systems/proper_int.ML \
+ ML-Systems/single_assignment.ML \
+ ML-Systems/single_assignment_polyml.ML \
+ ML-Systems/smlnj.ML \
+ ML-Systems/thread_dummy.ML \
+ ML-Systems/time_limit.ML \
+ ML-Systems/timing.ML \
+ ML-Systems/universal.ML \
+ ML-Systems/unsynchronized.ML \
+ ML-Systems/use_context.ML
RAW: $(OUT)/RAW
@@ -41,92 +55,205 @@
Pure: $(OUT)/Pure
-$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/cache.ML \
- Concurrent/future.ML Concurrent/lazy.ML \
- Concurrent/lazy_sequential.ML Concurrent/mailbox.ML \
- Concurrent/par_list.ML Concurrent/par_list_sequential.ML \
- Concurrent/simple_thread.ML Concurrent/single_assignment.ML \
- Concurrent/single_assignment_sequential.ML \
- Concurrent/synchronized.ML Concurrent/synchronized_sequential.ML \
- Concurrent/task_queue.ML General/alist.ML General/antiquote.ML \
- General/balanced_tree.ML General/basics.ML General/binding.ML \
- General/buffer.ML General/exn.ML General/file.ML General/graph.ML \
- General/heap.ML General/integer.ML General/long_name.ML \
- General/markup.ML General/name_space.ML General/ord_list.ML \
- General/output.ML General/path.ML General/position.ML \
- General/pretty.ML General/print_mode.ML General/properties.ML \
- General/queue.ML General/same.ML General/scan.ML General/sha1.ML \
- General/sha1_polyml.ML General/secure.ML General/seq.ML \
- General/source.ML General/stack.ML General/symbol.ML \
- General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML \
- General/xml_data.ML General/yxml.ML Isar/args.ML Isar/attrib.ML \
- Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \
- Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \
- Isar/context_rules.ML Isar/element.ML Isar/expression.ML \
- Isar/generic_target.ML Isar/isar_cmd.ML Isar/isar_document.ML \
- Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML \
- Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
- Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \
- Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML \
- Isar/parse_spec.ML Isar/parse_value.ML Isar/proof.ML \
- Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
- Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML \
- Isar/skip_proof.ML Isar/spec_rules.ML Isar/specification.ML \
- Isar/theory_target.ML Isar/token.ML Isar/toplevel.ML \
- Isar/typedecl.ML ML/ml_antiquote.ML ML/ml_compiler.ML \
- ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \
- ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \
- ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML \
- ML-Systems/use_context.ML Proof/extraction.ML PIDE/document.ML \
- Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
- Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML \
- ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \
- ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML \
- ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML \
- ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML \
- ProofGeneral/proof_general_emacs.ML General/yxml.ML Isar/args.ML \
- Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \
- Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \
- Isar/context_rules.ML Isar/element.ML Isar/expression.ML \
- Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML \
- Isar/keyword.ML Isar/local_defs.ML Isar/local_syntax.ML \
- Isar/local_theory.ML Isar/locale.ML Isar/method.ML \
- Isar/object_logic.ML Isar/obtain.ML Isar/outer_syntax.ML \
- Isar/overloading.ML Isar/parse.ML Isar/parse_spec.ML \
- Isar/parse_value.ML Isar/proof.ML Isar/proof_context.ML \
- Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
- Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML \
- Isar/spec_rules.ML Isar/specification.ML Isar/theory_target.ML \
- Isar/token.ML Isar/toplevel.ML Isar/typedecl.ML ML/ml_antiquote.ML \
- ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML \
- ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
- ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
- ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \
- Proof/extraction.ML PIDE/document.ML Proof/proof_rewrite_rules.ML \
- Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
- ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
- ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \
- ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \
- ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \
- ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML \
- ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \
- Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
- Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \
- Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML \
- System/isabelle_process.ML System/isar.ML System/session.ML \
- Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML \
- Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \
- Thy/thy_output.ML Thy/thy_syntax.ML Tools/find_consts.ML \
- Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML \
- assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \
- consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \
- drule.ML envir.ML facts.ML goal.ML goal_display.ML interpretation.ML \
- item_net.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \
- morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML \
- primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML \
- sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tactical.ML \
- term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML \
- type_infer.ML unify.ML variable.ML
+$(OUT)/Pure: $(BOOTSTRAP_FILES) \
+ Concurrent/cache.ML \
+ Concurrent/future.ML \
+ Concurrent/lazy.ML \
+ Concurrent/lazy_sequential.ML \
+ Concurrent/mailbox.ML \
+ Concurrent/par_list.ML \
+ Concurrent/par_list_sequential.ML \
+ Concurrent/simple_thread.ML \
+ Concurrent/single_assignment.ML \
+ Concurrent/single_assignment_sequential.ML \
+ Concurrent/synchronized.ML \
+ Concurrent/synchronized_sequential.ML \
+ Concurrent/task_queue.ML \
+ General/alist.ML \
+ General/antiquote.ML \
+ General/balanced_tree.ML \
+ General/basics.ML \
+ General/binding.ML \
+ General/buffer.ML \
+ General/exn.ML \
+ General/file.ML \
+ General/graph.ML \
+ General/heap.ML \
+ General/integer.ML \
+ General/long_name.ML \
+ General/markup.ML \
+ General/name_space.ML \
+ General/ord_list.ML \
+ General/output.ML \
+ General/path.ML \
+ General/position.ML \
+ General/pretty.ML \
+ General/print_mode.ML \
+ General/properties.ML \
+ General/queue.ML \
+ General/same.ML \
+ General/scan.ML \
+ General/secure.ML \
+ General/seq.ML \
+ General/sha1.ML \
+ General/sha1_polyml.ML \
+ General/source.ML \
+ General/stack.ML \
+ General/symbol.ML \
+ General/symbol_pos.ML \
+ General/table.ML \
+ General/url.ML \
+ General/xml.ML \
+ General/xml_data.ML \
+ General/yxml.ML \
+ Isar/args.ML \
+ Isar/attrib.ML \
+ Isar/auto_bind.ML \
+ Isar/calculation.ML \
+ Isar/class.ML \
+ Isar/class_target.ML \
+ Isar/code.ML \
+ Isar/constdefs.ML \
+ Isar/context_rules.ML \
+ Isar/element.ML \
+ Isar/expression.ML \
+ Isar/generic_target.ML \
+ Isar/isar_cmd.ML \
+ Isar/isar_document.ML \
+ Isar/isar_syn.ML \
+ Isar/keyword.ML \
+ Isar/local_defs.ML \
+ Isar/local_syntax.ML \
+ Isar/local_theory.ML \
+ Isar/locale.ML \
+ Isar/method.ML \
+ Isar/object_logic.ML \
+ Isar/obtain.ML \
+ Isar/outer_syntax.ML \
+ Isar/overloading.ML \
+ Isar/parse.ML \
+ Isar/parse_spec.ML \
+ Isar/parse_value.ML \
+ Isar/proof.ML \
+ Isar/proof_context.ML \
+ Isar/proof_display.ML \
+ Isar/proof_node.ML \
+ Isar/rule_cases.ML \
+ Isar/rule_insts.ML \
+ Isar/runtime.ML \
+ Isar/skip_proof.ML \
+ Isar/spec_rules.ML \
+ Isar/specification.ML \
+ Isar/theory_target.ML \
+ Isar/token.ML \
+ Isar/toplevel.ML \
+ Isar/typedecl.ML \
+ ML/install_pp_polyml-5.3.ML \
+ ML/install_pp_polyml.ML \
+ ML/ml_antiquote.ML \
+ ML/ml_compiler.ML \
+ ML/ml_compiler_polyml-5.3.ML \
+ ML/ml_context.ML \
+ ML/ml_env.ML \
+ ML/ml_lex.ML \
+ ML/ml_parse.ML \
+ ML/ml_syntax.ML \
+ ML/ml_thms.ML \
+ PIDE/document.ML \
+ Proof/extraction.ML \
+ Proof/proof_rewrite_rules.ML \
+ Proof/proof_syntax.ML \
+ Proof/proofchecker.ML \
+ Proof/reconstruct.ML \
+ ProofGeneral/pgip.ML \
+ ProofGeneral/pgip_input.ML \
+ ProofGeneral/pgip_isabelle.ML \
+ ProofGeneral/pgip_markup.ML \
+ ProofGeneral/pgip_output.ML \
+ ProofGeneral/pgip_parser.ML \
+ ProofGeneral/pgip_tests.ML \
+ ProofGeneral/pgip_types.ML \
+ ProofGeneral/pgml.ML \
+ ProofGeneral/preferences.ML \
+ ProofGeneral/proof_general_emacs.ML \
+ ProofGeneral/proof_general_pgip.ML \
+ Pure.thy \
+ ROOT.ML \
+ Syntax/ast.ML \
+ Syntax/lexicon.ML \
+ Syntax/mixfix.ML \
+ Syntax/parser.ML \
+ Syntax/printer.ML \
+ Syntax/simple_syntax.ML \
+ Syntax/syn_ext.ML \
+ Syntax/syn_trans.ML \
+ Syntax/syntax.ML \
+ Syntax/type_ext.ML \
+ System/isabelle_process.ML \
+ System/isar.ML \
+ System/session.ML \
+ Thy/html.ML \
+ Thy/latex.ML \
+ Thy/present.ML \
+ Thy/term_style.ML \
+ Thy/thm_deps.ML \
+ Thy/thy_header.ML \
+ Thy/thy_info.ML \
+ Thy/thy_load.ML \
+ Thy/thy_output.ML \
+ Thy/thy_syntax.ML \
+ Tools/find_consts.ML \
+ Tools/find_theorems.ML \
+ Tools/named_thms.ML \
+ Tools/xml_syntax.ML \
+ assumption.ML \
+ axclass.ML \
+ codegen.ML \
+ config.ML \
+ conjunction.ML \
+ consts.ML \
+ context.ML \
+ context_position.ML \
+ conv.ML \
+ defs.ML \
+ display.ML \
+ drule.ML \
+ envir.ML \
+ facts.ML \
+ goal.ML \
+ goal_display.ML \
+ interpretation.ML \
+ item_net.ML \
+ library.ML \
+ logic.ML \
+ meta_simplifier.ML \
+ more_thm.ML \
+ morphism.ML \
+ name.ML \
+ net.ML \
+ old_goals.ML \
+ old_term.ML \
+ pattern.ML \
+ primitive_defs.ML \
+ proofterm.ML \
+ pure_setup.ML \
+ pure_thy.ML \
+ search.ML \
+ sign.ML \
+ simplifier.ML \
+ sorts.ML \
+ subgoal.ML \
+ tactic.ML \
+ tactical.ML \
+ term.ML \
+ term_ord.ML \
+ term_subst.ML \
+ theory.ML \
+ thm.ML \
+ type.ML \
+ type_infer.ML \
+ unify.ML \
+ variable.ML
@./mk
@@ -141,5 +268,4 @@
## clean
clean:
- @rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz \
- $(LOG)/Pure-ProofGeneral.gz
+ @rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz $(LOG)/Pure-ProofGeneral.gz
--- a/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Wed Aug 11 12:50:33 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML
-
-Extra toplevel pretty-printing for Poly/ML 5.3.0.
-*)
-
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
- pretty (Synchronized.value var, depth));
-
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
- (case Future.peek x of
- NONE => PolyML.PrettyString "<future>"
- | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
- | SOME (Exn.Result y) => pretty (y, depth)));
-
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
- (case Lazy.peek x of
- NONE => PolyML.PrettyString "<lazy>"
- | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
- | SOME (Exn.Result y) => pretty (y, depth)));
-
-PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
- let
- open PolyML;
- val from_ML = Pretty.from_ML o pretty_ml;
- fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
- fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
- fun prt_term parens dp (t as _ $ _) =
- op :: (strip_comb t)
- |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
- |> Pretty.separate " $"
- |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
- | prt_term _ dp (Abs (x, T, body)) =
- prt_apps "Abs"
- [from_ML (prettyRepresentation (x, dp - 1)),
- from_ML (prettyRepresentation (T, dp - 2)),
- prt_term false (dp - 3) body]
- | prt_term _ dp (Const const) =
- prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
- | prt_term _ dp (Free free) =
- prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
- | prt_term _ dp (Var var) =
- prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
- | prt_term _ dp (Bound i) =
- prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
- in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
-
--- a/src/Pure/ML-Systems/install_pp_polyml.ML Wed Aug 11 12:50:33 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: Pure/ML-Systems/install_pp_polyml.ML
-
-Extra toplevel pretty-printing for Poly/ML.
-*)
-
-PolyML.install_pp
- (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
- (case Future.peek x of
- NONE => str "<future>"
- | SOME (Exn.Exn _) => str "<failed>"
- | SOME (Exn.Result y) => print (y, depth)));
-
-PolyML.install_pp
- (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
- (case Lazy.peek x of
- NONE => str "<lazy>"
- | SOME (Exn.Exn _) => str "<failed>"
- | SOME (Exn.Result y) => print (y, depth)));
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/install_pp_polyml-5.3.ML Wed Aug 11 13:39:36 2010 +0200
@@ -0,0 +1,47 @@
+(* Title: Pure/ML/install_pp_polyml-5.3.ML
+ Author: Makarius
+
+Extra toplevel pretty-printing for Poly/ML 5.3.0.
+*)
+
+PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
+ pretty (Synchronized.value var, depth));
+
+PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+ (case Future.peek x of
+ NONE => PolyML.PrettyString "<future>"
+ | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+ | SOME (Exn.Result y) => pretty (y, depth)));
+
+PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+ (case Lazy.peek x of
+ NONE => PolyML.PrettyString "<lazy>"
+ | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+ | SOME (Exn.Result y) => pretty (y, depth)));
+
+PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
+ let
+ open PolyML;
+ val from_ML = Pretty.from_ML o pretty_ml;
+ fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
+ fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
+ fun prt_term parens dp (t as _ $ _) =
+ op :: (strip_comb t)
+ |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
+ |> Pretty.separate " $"
+ |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
+ | prt_term _ dp (Abs (x, T, body)) =
+ prt_apps "Abs"
+ [from_ML (prettyRepresentation (x, dp - 1)),
+ from_ML (prettyRepresentation (T, dp - 2)),
+ prt_term false (dp - 3) body]
+ | prt_term _ dp (Const const) =
+ prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
+ | prt_term _ dp (Free free) =
+ prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
+ | prt_term _ dp (Var var) =
+ prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
+ | prt_term _ dp (Bound i) =
+ prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
+ in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/install_pp_polyml.ML Wed Aug 11 13:39:36 2010 +0200
@@ -0,0 +1,20 @@
+(* Title: Pure/ML/install_pp_polyml.ML
+ Author: Makarius
+
+Extra toplevel pretty-printing for Poly/ML.
+*)
+
+PolyML.install_pp
+ (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
+ (case Future.peek x of
+ NONE => str "<future>"
+ | SOME (Exn.Exn _) => str "<failed>"
+ | SOME (Exn.Result y) => print (y, depth)));
+
+PolyML.install_pp
+ (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
+ (case Lazy.peek x of
+ NONE => str "<lazy>"
+ | SOME (Exn.Exn _) => str "<failed>"
+ | SOME (Exn.Result y) => print (y, depth)));
+
--- a/src/Pure/pure_setup.ML Wed Aug 11 12:50:33 2010 +0200
+++ b/src/Pure/pure_setup.ML Wed Aug 11 13:39:36 2010 +0200
@@ -40,9 +40,9 @@
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
if ml_system = "polyml-5.3.0"
-then use "ML-Systems/install_pp_polyml-5.3.ML"
+then use "ML/install_pp_polyml-5.3.ML"
else if String.isPrefix "polyml" ml_system
-then use "ML-Systems/install_pp_polyml.ML"
+then use "ML/install_pp_polyml.ML"
else ();
if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then