# HG changeset patch
# User wenzelm
# Date 1244135754 -7200
# Node ID 12f5f6af3d2d8518bad3512869682d4bdf922ecc
# Parent  9858f32f95696c7c60d42fea7165e89fa1d6ca7a
less experimental polyml-5.3;

diff -r 9858f32f9569 -r 12f5f6af3d2d src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Jun 04 18:00:47 2009 +0200
+++ b/src/Pure/IsaMakefile	Thu Jun 04 19:15:54 2009 +0200
@@ -68,15 +68,14 @@
   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-experimental.ML				\
-  ML-Systems/use_context.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/preferences.ML		\
-  ProofGeneral/proof_general_emacs.ML					\
+  ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.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/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		\
diff -r 9858f32f9569 -r 12f5f6af3d2d src/Pure/ML-Systems/compiler_polyml-5.3.ML
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Thu Jun 04 18:00:47 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Thu Jun 04 19:15:54 2009 +0200
@@ -1,6 +1,6 @@
 (*  Title:      Pure/ML-Systems/compiler_polyml-5.3.ML
 
-Runtime compilation for Poly/ML 5.3 (SVN experimental).
+Runtime compilation for Poly/ML 5.3.
 *)
 
 local
diff -r 9858f32f9569 -r 12f5f6af3d2d src/Pure/ML-Systems/install_pp_polyml-5.3.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/install_pp_polyml-5.3.ML	Thu Jun 04 19:15:54 2009 +0200
@@ -0,0 +1,17 @@
+(*  Title:      Pure/ML-Systems/install_pp_polyml-5.3.ML
+
+Extra toplevel pretty-printing for Poly/ML 5.3.
+*)
+
+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)));
+
diff -r 9858f32f9569 -r 12f5f6af3d2d src/Pure/ML-Systems/install_pp_polyml-experimental.ML
--- a/src/Pure/ML-Systems/install_pp_polyml-experimental.ML	Thu Jun 04 18:00:47 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      Pure/ML-Systems/install_pp_polyml-experimental.ML
-
-Extra toplevel pretty-printing for Poly/ML 5.3 (SVN experimental).
-*)
-
-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)));
-
diff -r 9858f32f9569 -r 12f5f6af3d2d src/Pure/ML-Systems/polyml-experimental.ML
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Thu Jun 04 18:00:47 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Thu Jun 04 19:15:54 2009 +0200
@@ -1,6 +1,6 @@
 (*  Title:      Pure/ML-Systems/polyml-experimental.ML
 
-Compatibility wrapper for Poly/ML 5.3 (SVN experimental).
+Compatibility wrapper for Poly/ML 5.3.
 *)
 
 open Thread;
diff -r 9858f32f9569 -r 12f5f6af3d2d src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Thu Jun 04 18:00:47 2009 +0200
+++ b/src/Pure/pure_setup.ML	Thu Jun 04 19:15:54 2009 +0200
@@ -42,8 +42,8 @@
 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
 
-if File.exists (Path.explode ("ML-Systems/install_pp_" ^ ml_system ^ ".ML"))
-then use ("ML-Systems/install_pp_" ^ ml_system ^ ".ML")
+if ml_system = "polyml-experimental"
+then use "ML-Systems/install_pp_polyml-5.3.ML"
 else if String.isPrefix "polyml" ml_system
 then use "ML-Systems/install_pp_polyml.ML"
 else ();