# HG changeset patch
# User wenzelm
# Date 1190634771 -7200
# Node ID ac5b5a6155ddb79f22fda6b263c1fa60076cb496
# Parent  a5754ca5c5107c42577639026bb580c79ccce638
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);

diff -r a5754ca5c510 -r ac5b5a6155dd src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon Sep 24 13:52:50 2007 +0200
+++ b/src/Pure/IsaMakefile	Mon Sep 24 13:52:51 2007 +0200
@@ -45,24 +45,23 @@
   Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML				\
   Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML			\
   ML-Systems/alice.ML ML-Systems/exn.ML						\
-  ML-Systems/multithreading_dummy.ML ML-Systems/multithreading_polyml.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-interrupt-timeout.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/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/parsing.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			\
+  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/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/parsing.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 Thy/html.ML Thy/latex.ML Thy/present.ML			\
   Thy/term_style.ML Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_edit.ML		\
   Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML		\
@@ -82,13 +81,13 @@
 
 RAW: $(OUT)/RAW
 
-$(OUT)/RAW: ML-Systems/alice.ML ML-Systems/exn.ML 				\
-  ML-Systems/multithreading_dummy.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-interrupt-timeout.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
+$(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
 	@./mk -r