# HG changeset patch
# User wenzelm
# Date 1281526776 -7200
# Node ID d6afb77b0f6daee82c1451a49e2bce0fa0a95d50
# Parent  01d2ef471ffe979e741f5f35a0183e0f3eb98088
more precise and more maintainable dependencies;

diff -r 01d2ef471ffe -r d6afb77b0f6d src/Pure/IsaMakefile
--- 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
diff -r 01d2ef471ffe -r d6afb77b0f6d src/Pure/ML-Systems/install_pp_polyml-5.3.ML
--- 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);
-
diff -r 01d2ef471ffe -r d6afb77b0f6d src/Pure/ML-Systems/install_pp_polyml.ML
--- 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)));
-
diff -r 01d2ef471ffe -r d6afb77b0f6d src/Pure/ML/install_pp_polyml-5.3.ML
--- /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);
+
diff -r 01d2ef471ffe -r d6afb77b0f6d src/Pure/ML/install_pp_polyml.ML
--- /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)));
+
diff -r 01d2ef471ffe -r d6afb77b0f6d src/Pure/pure_setup.ML
--- 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