# HG changeset patch
# User wenzelm
# Date 1244131247 -7200
# Node ID 9858f32f95696c7c60d42fea7165e89fa1d6ca7a
# Parent  6b840c0b7fb6794f2717bf521335fabe37fad9fa
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;

diff -r 6b840c0b7fb6 -r 9858f32f9569 src/Pure/Concurrent/ROOT.ML
--- a/src/Pure/Concurrent/ROOT.ML	Thu Jun 04 17:31:39 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(*  Title:      Pure/Concurrent/ROOT.ML
-    Author:     Makarius
-
-Concurrency within the ML runtime.
-*)
-
-use "simple_thread.ML";
-use "synchronized.ML";
-use "mailbox.ML";
-use "task_queue.ML";
-use "future.ML";
-use "par_list.ML";
-if Multithreading.available then () else use "par_list_dummy.ML";
-
diff -r 6b840c0b7fb6 -r 9858f32f9569 src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Thu Jun 04 17:31:39 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(*  Title:      Pure/General/ROOT.ML
-
-Library of general tools.
-*)
-
-use "print_mode.ML";
-use "alist.ML";
-use "table.ML";
-use "output.ML";
-use "properties.ML";
-use "markup.ML";
-use "scan.ML";
-use "source.ML";
-use "symbol.ML";
-use "seq.ML";
-use "position.ML";
-use "symbol_pos.ML";
-use "antiquote.ML";
-use "../ML/ml_lex.ML";
-use "../ML/ml_parse.ML";
-use "secure.ML";
-
-use "integer.ML";
-use "stack.ML";
-use "queue.ML";
-use "heap.ML";
-use "ord_list.ML";
-use "balanced_tree.ML";
-use "graph.ML";
-use "long_name.ML";
-use "binding.ML";
-use "name_space.ML";
-use "lazy.ML";
-use "path.ML";
-use "url.ML";
-use "buffer.ML";
-use "file.ML";
-use "xml.ML";
-use "yxml.ML";
-
diff -r 6b840c0b7fb6 -r 9858f32f9569 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Jun 04 17:31:39 2009 +0200
+++ b/src/Pure/IsaMakefile	Thu Jun 04 18:00:47 2009 +0200
@@ -39,45 +39,44 @@
 
 Pure: $(OUT)/Pure
 
-$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/ROOT.ML			\
-  Concurrent/future.ML Concurrent/mailbox.ML Concurrent/par_list.ML	\
+$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/future.ML			\
+  Concurrent/mailbox.ML Concurrent/par_list.ML				\
   Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
-  Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML	\
-  General/alist.ML General/antiquote.ML General/balanced_tree.ML	\
-  General/basics.ML General/binding.ML General/buffer.ML		\
-  General/file.ML General/graph.ML General/heap.ML General/integer.ML	\
-  General/lazy.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/scan.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/yxml.ML	\
-  Isar/ROOT.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/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_keyword.ML		\
-  Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
-  Isar/overloading.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/skip_proof.ML Isar/spec_parse.ML		\
-  Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML		\
-  Isar/value_parse.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					\
+  Concurrent/synchronized.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/file.ML			\
+  General/graph.ML General/heap.ML General/integer.ML General/lazy.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/scan.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/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/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_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML		\
+  Isar/outer_syntax.ML Isar/overloading.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/skip_proof.ML		\
+  Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML	\
+  Isar/toplevel.ML Isar/value_parse.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-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/ROOT.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	\
+  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		\
@@ -85,17 +84,17 @@
   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/ROOT.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			\
-  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		\
-  tctical.ML term.ML term_ord.ML term_subst.ML theory.ML thm.ML		\
-  type.ML type_infer.ML unify.ML variable.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 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 tctical.ML term.ML	\
+  term_ord.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML	\
+  unify.ML variable.ML
 	@./mk
 
 
diff -r 6b840c0b7fb6 -r 9858f32f9569 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Thu Jun 04 17:31:39 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,95 +0,0 @@
-(*  Title:      Pure/Isar/ROOT.ML
-    Author:     Markus Wenzel, TU Muenchen
-
-Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
-*)
-
-(*proof context*)
-use "object_logic.ML";
-use "rule_cases.ML";
-use "auto_bind.ML";
-use "local_syntax.ML";
-use "proof_context.ML";
-use "local_defs.ML";
-
-(*proof term operations*)
-use "../Proof/reconstruct.ML";
-use "../Proof/proof_syntax.ML";
-use "../Proof/proof_rewrite_rules.ML";
-use "../Proof/proofchecker.ML";
-
-(*outer syntax*)
-use "outer_lex.ML";
-use "outer_keyword.ML";
-use "outer_parse.ML";
-use "value_parse.ML";
-use "args.ML";
-
-(*ML support*)
-use "../ML/ml_syntax.ML";
-use "../ML/ml_env.ML";
-if ml_system = "polyml-experimental"
-then use "../ML/ml_compiler_polyml-5.3.ML"
-else use "../ML/ml_compiler.ML";
-use "../ML/ml_context.ML";
-
-(*theory sources*)
-use "../Thy/thy_header.ML";
-use "../Thy/thy_load.ML";
-use "../Thy/html.ML";
-use "../Thy/latex.ML";
-use "../Thy/present.ML";
-
-(*basic proof engine*)
-use "proof_display.ML";
-use "attrib.ML";
-use "../ML/ml_antiquote.ML";
-use "context_rules.ML";
-use "skip_proof.ML";
-use "method.ML";
-use "proof.ML";
-use "../ML/ml_thms.ML";
-use "element.ML";
-
-(*derived theory and proof elements*)
-use "calculation.ML";
-use "obtain.ML";
-
-(*local theories and targets*)
-use "local_theory.ML";
-use "overloading.ML";
-use "locale.ML";
-use "class_target.ML";
-use "theory_target.ML";
-use "expression.ML";
-use "class.ML";
-
-(*complex proof machineries*)
-use "../simplifier.ML";
-
-(*executable theory content*)
-use "code.ML";
-
-(*specifications*)
-use "spec_parse.ML";
-use "specification.ML";
-use "constdefs.ML";
-
-(*toplevel transactions*)
-use "proof_node.ML";
-use "toplevel.ML";
-
-(*theory syntax*)
-use "../Thy/term_style.ML";
-use "../Thy/thy_output.ML";
-use "../Thy/thy_syntax.ML";
-use "../old_goals.ML";
-use "outer_syntax.ML";
-use "../Thy/thy_info.ML";
-use "isar_document.ML";
-
-(*theory and proof operations*)
-use "rule_insts.ML";
-use "../Thy/thm_deps.ML";
-use "isar_cmd.ML";
-use "isar_syn.ML";
diff -r 6b840c0b7fb6 -r 9858f32f9569 src/Pure/ProofGeneral/ROOT.ML
--- a/src/Pure/ProofGeneral/ROOT.ML	Thu Jun 04 17:31:39 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*  Title:      Pure/ProofGeneral/ROOT.ML
-    Author:     David Aspinall
-
-Proof General interface for Isabelle, both the traditional Emacs version,
-and PGIP experiments.
-*)
-
-use "pgip_types.ML";
-use "pgml.ML";
-use "pgip_markup.ML";
-use "pgip_input.ML";
-use "pgip_output.ML";
-use "pgip.ML";
-
-use "pgip_isabelle.ML";
-
-use "preferences.ML";
-
-use "pgip_parser.ML";
-
-use "pgip_tests.ML";
-
-use "proof_general_pgip.ML";
-use "proof_general_emacs.ML";
-
diff -r 6b840c0b7fb6 -r 9858f32f9569 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jun 04 17:31:39 2009 +0200
+++ b/src/Pure/ROOT.ML	Thu Jun 04 18:00:47 2009 +0200
@@ -1,4 +1,4 @@
-(* Pure Isabelle *)
+(** Pure Isabelle **)
 
 structure Distribution =     (*filled-in by makedist*)
 struct
@@ -12,14 +12,60 @@
 
 print_depth 10;
 
-(*basic tools*)
+
+(* library of general tools *)
+
 use "General/basics.ML";
 use "library.ML";
+use "General/print_mode.ML";
+use "General/alist.ML";
+use "General/table.ML";
+use "General/output.ML";
+use "General/properties.ML";
+use "General/markup.ML";
+use "General/scan.ML";
+use "General/source.ML";
+use "General/symbol.ML";
+use "General/seq.ML";
+use "General/position.ML";
+use "General/symbol_pos.ML";
+use "General/antiquote.ML";
+use "ML/ml_lex.ML";
+use "ML/ml_parse.ML";
+use "General/secure.ML";
+(*----- basic ML bootstrap finished -----*)
+use "General/integer.ML";
+use "General/stack.ML";
+use "General/queue.ML";
+use "General/heap.ML";
+use "General/ord_list.ML";
+use "General/balanced_tree.ML";
+use "General/graph.ML";
+use "General/long_name.ML";
+use "General/binding.ML";
+use "General/name_space.ML";
+use "General/lazy.ML";
+use "General/path.ML";
+use "General/url.ML";
+use "General/buffer.ML";
+use "General/file.ML";
+use "General/xml.ML";
+use "General/yxml.ML";
 
-cd "General"; use "ROOT.ML"; cd "..";
-cd "Concurrent"; use "ROOT.ML"; cd "..";
+
+(* concurrency within the ML runtime *)
 
-(*fundamental structures*)
+use "Concurrent/simple_thread.ML";
+use "Concurrent/synchronized.ML";
+use "Concurrent/mailbox.ML";
+use "Concurrent/task_queue.ML";
+use "Concurrent/future.ML";
+use "Concurrent/par_list.ML";
+if Multithreading.available then () else use "Concurrent/par_list_dummy.ML";
+
+
+(* fundamental structures *)
+
 use "name.ML";
 use "term.ML";
 use "term_ord.ML";
@@ -35,7 +81,9 @@
 use "type.ML";
 use "config.ML";
 
-(*inner syntax module*)
+
+(* inner syntax *)
+
 use "Syntax/ast.ML";
 use "Syntax/syn_ext.ML";
 use "Syntax/parser.ML";
@@ -47,7 +95,9 @@
 
 use "type_infer.ML";
 
-(*core of tactical proof system*)
+
+(* core of tactical proof system *)
+
 use "net.ML";
 use "item_net.ML";
 use "envir.ML";
@@ -78,24 +128,142 @@
 use "goal.ML";
 use "axclass.ML";
 
-(*main Isar stuff*)
-cd "Isar"; use "ROOT.ML"; cd "..";
+
+(* Isar -- Intelligible Semi-Automated Reasoning *)
+
+(*proof context*)
+use "Isar/object_logic.ML";
+use "Isar/rule_cases.ML";
+use "Isar/auto_bind.ML";
+use "Isar/local_syntax.ML";
+use "Isar/proof_context.ML";
+use "Isar/local_defs.ML";
+
+(*proof term operations*)
+use "Proof/reconstruct.ML";
+use "Proof/proof_syntax.ML";
+use "Proof/proof_rewrite_rules.ML";
+use "Proof/proofchecker.ML";
+
+(*outer syntax*)
+use "Isar/outer_lex.ML";
+use "Isar/outer_keyword.ML";
+use "Isar/outer_parse.ML";
+use "Isar/value_parse.ML";
+use "Isar/args.ML";
+
+(*ML support*)
+use "ML/ml_syntax.ML";
+use "ML/ml_env.ML";
+if ml_system = "polyml-experimental"
+then use "ML/ml_compiler_polyml-5.3.ML"
+else use "ML/ml_compiler.ML";
+use "ML/ml_context.ML";
+
+(*theory sources*)
+use "Thy/thy_header.ML";
+use "Thy/thy_load.ML";
+use "Thy/html.ML";
+use "Thy/latex.ML";
+use "Thy/present.ML";
+
+(*basic proof engine*)
+use "Isar/proof_display.ML";
+use "Isar/attrib.ML";
+use "ML/ml_antiquote.ML";
+use "Isar/context_rules.ML";
+use "Isar/skip_proof.ML";
+use "Isar/method.ML";
+use "Isar/proof.ML";
+use "ML/ml_thms.ML";
+use "Isar/element.ML";
+
+(*derived theory and proof elements*)
+use "Isar/calculation.ML";
+use "Isar/obtain.ML";
+
+(*local theories and targets*)
+use "Isar/local_theory.ML";
+use "Isar/overloading.ML";
+use "Isar/locale.ML";
+use "Isar/class_target.ML";
+use "Isar/theory_target.ML";
+use "Isar/expression.ML";
+use "Isar/class.ML";
+
+use "simplifier.ML";
+
+(*executable theory content*)
+use "Isar/code.ML";
+
+(*specifications*)
+use "Isar/spec_parse.ML";
+use "Isar/specification.ML";
+use "Isar/constdefs.ML";
+
+(*toplevel transactions*)
+use "Isar/proof_node.ML";
+use "Isar/toplevel.ML";
+
+(*theory syntax*)
+use "Thy/term_style.ML";
+use "Thy/thy_output.ML";
+use "Thy/thy_syntax.ML";
+use "old_goals.ML";
+use "Isar/outer_syntax.ML";
+use "Thy/thy_info.ML";
+use "Isar/isar_document.ML";
+
+(*theory and proof operations*)
+use "Isar/rule_insts.ML";
+use "Thy/thm_deps.ML";
+use "Isar/isar_cmd.ML";
+use "Isar/isar_syn.ML";
+
 use "subgoal.ML";
 
 use "Proof/extraction.ML";
 
-(*Isabelle/Isar system*)
+
+(* Isabelle/Isar system *)
+
 use "System/session.ML";
 use "System/isar.ML";
 use "System/isabelle_process.ML";
 
-(*additional tools*)
-cd "Tools"; use "ROOT.ML"; cd "..";
+
+(* miscellaneous tools and packages for Pure Isabelle *)
+
+use "Tools/named_thms.ML";
+
+use "Tools/xml_syntax.ML";
+
+use "Tools/find_theorems.ML";
+use "Tools/find_consts.ML";
 
 use "codegen.ML";
 
-(*configuration for Proof General*)
-cd "ProofGeneral"; use "ROOT.ML"; cd "..";
+
+(* configuration for Proof General *)
+
+use "ProofGeneral/pgip_types.ML";
+use "ProofGeneral/pgml.ML";
+use "ProofGeneral/pgip_markup.ML";
+use "ProofGeneral/pgip_input.ML";
+use "ProofGeneral/pgip_output.ML";
+use "ProofGeneral/pgip.ML";
+
+use "ProofGeneral/pgip_isabelle.ML";
+
+use "ProofGeneral/preferences.ML";
+
+use "ProofGeneral/pgip_parser.ML";
+
+use "ProofGeneral/pgip_tests.ML";
+
+use "ProofGeneral/proof_general_pgip.ML";
+use "ProofGeneral/proof_general_emacs.ML";
+
 
 use "pure_setup.ML";
 
diff -r 6b840c0b7fb6 -r 9858f32f9569 src/Pure/Tools/ROOT.ML
--- a/src/Pure/Tools/ROOT.ML	Thu Jun 04 17:31:39 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(* Miscellaneous tools and packages for Pure Isabelle *)
-
-use "named_thms.ML";
-
-use "xml_syntax.ML";
-
-use "find_theorems.ML";
-use "find_consts.ML";
-