# HG changeset patch
# User wenzelm
# Date 1204827685 -3600
# Node ID 73ed8cb8ac4dee28b3cd0f12f57f55047978df58
# Parent  3a190cb91c6cd869d671b98b2b8176f0e2d5a85e
cleaned-up ML-Systems;

diff -r 3a190cb91c6c -r 73ed8cb8ac4d src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Mar 06 19:21:24 2008 +0100
+++ b/src/Pure/IsaMakefile	Thu Mar 06 19:21:25 2008 +0100
@@ -23,18 +23,17 @@
 
 Pure: $(OUT)/Pure$(ML_SUFFIX)
 
-$(OUT)/Pure$(ML_SUFFIX): \
-  CPure.thy General/ROOT.ML General/alist.ML General/balanced_tree.ML	\
-  General/basics.ML General/buffer.ML General/file.ML General/graph.ML	\
-  General/heap.ML General/history.ML General/integer.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/scan.ML		\
-  General/secure.ML General/seq.ML General/source.ML General/stack.ML	\
-  General/susp.ML General/symbol.ML General/table.ML General/url.ML	\
-  General/xml.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML		\
-  Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML	\
-  Isar/code.ML Isar/code_unit.ML Isar/constdefs.ML			\
+$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML	\
+  General/balanced_tree.ML General/basics.ML General/buffer.ML		\
+  General/file.ML General/graph.ML General/heap.ML General/history.ML	\
+  General/integer.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/scan.ML General/secure.ML General/seq.ML General/source.ML	\
+  General/stack.ML General/susp.ML General/symbol.ML General/table.ML	\
+  General/url.ML General/xml.ML Isar/ROOT.ML Isar/antiquote.ML		\
+  Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML	\
+  Isar/class.ML Isar/code.ML Isar/code_unit.ML Isar/constdefs.ML	\
   Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML		\
   Isar/instance.ML Isar/isar_cmd.ML Isar/isar_syn.ML			\
   Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\
@@ -48,14 +47,14 @@
   ML-Systems/alice.ML ML-Systems/exn.ML ML-Systems/multithreading.ML	\
   ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML	\
   ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML			\
-  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML			\
-  ML-Systems/polyml-old-basis.ML ML-Systems/polyml-posix.ML		\
-  ML-Systems/polyml.ML ML-Systems/poplogml.ML ML-Systems/proper_int.ML	\
-  ML-Systems/smlnj.ML ML-Systems/time_limit.ML ML-Systems/universal.ML	\
-  ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.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	\
+  ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML			\
+  ML-Systems/polyml_common.ML ML-Systems/polyml.ML			\
+  ML-Systems/poplogml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML	\
+  ML-Systems/time_limit.ML ML-Systems/universal.ML ML/ml_context.ML	\
+  ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.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			\
@@ -90,13 +89,13 @@
 
 RAW: $(OUT)/RAW
 
-$(OUT)/RAW: ML-Systems/alice.ML ML-Systems/exn.ML ML-Systems/multithreading.ML	\
-  ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML		\
-  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML				\
-  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML				\
-  ML-Systems/polyml-old-basis.ML ML-Systems/polyml-posix.ML			\
-  ML-Systems/polyml.ML ML-Systems/poplogml.ML ML-Systems/proper_int.ML		\
-  ML-Systems/smlnj.ML ML-Systems/time_limit.ML
+$(OUT)/RAW: ML-Systems/alice.ML ML-Systems/exn.ML			\
+  ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML	\
+  ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML		\
+  ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML			\
+  ML-Systems/polyml-5.0.ML ML-Systems/polyml_common.ML			\
+  ML-Systems/polyml.ML ML-Systems/poplogml.ML ML-Systems/proper_int.ML	\
+  ML-Systems/smlnj.ML ML-Systems/time_limit.ML ML-Systems/universal.ML
 	@./mk -r