# HG changeset patch
# User wenzelm
# Date 1456759792 -3600
# Node ID 01e2bd5b40270e535eb0e2b0210721c64d720d78
# Parent  e3f3854f460efe9ef9a2bd7125de0ab52ce651e7
tuned;

diff -r e3f3854f460e -r 01e2bd5b4027 src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Mon Feb 29 16:25:51 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Mon Feb 29 16:29:52 2016 +0100
@@ -171,8 +171,8 @@
 PolyML.Compiler.reportUnreferencedIds := true;
 PolyML.Compiler.printInAlphabeticalOrder := false;
 PolyML.Compiler.maxInlineSize := 80;
-
-fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
+PolyML.Compiler.prompt1 := "ML> ";
+PolyML.Compiler.prompt2 := "ML# ";
 
 use "RAW/ml_parse_tree.ML";
 if ML_System.name = "polyml-5.6"
diff -r e3f3854f460e -r 01e2bd5b4027 src/Pure/build
--- a/src/Pure/build	Mon Feb 29 16:25:51 2016 +0100
+++ b/src/Pure/build	Mon Feb 29 16:29:52 2016 +0100
@@ -68,7 +68,6 @@
     "$ISABELLE_PROCESS" \
       -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
       -e "structure Isar = struct fun main () = () end;" \
-      -e "ml_prompts \"ML> \" \"ML# \";" \
       -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
       -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
   fi
@@ -81,7 +80,6 @@
     rm -f "$OUTPUT"
     "$ISABELLE_PROCESS" \
       -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
-      -e "ml_prompts \"ML> \" \"ML# \";" \
       -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
       -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
   fi