# HG changeset patch
# User wenzelm
# Date 1198181518 -3600
# Node ID 308315ee2b6d4030c1a4f579c66815e33f1949d7
# Parent  b3e415b0cf5c13a5a96ee6debb2e015c0f20474d
added ML-Systems/universal.ML;

diff -r b3e415b0cf5c -r 308315ee2b6d src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Dec 20 21:09:38 2007 +0100
+++ b/src/Pure/IsaMakefile	Thu Dec 20 21:11:58 2007 +0100
@@ -26,31 +26,32 @@
 $(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 Isar/locale.ML Isar/method.ML Isar/net_rules.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/proof.ML Isar/proof_context.ML Isar/proof_display.ML			\
-  Isar/proof_history.ML Isar/rule_cases.ML Isar/rule_insts.ML			\
-  Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML				\
-  Isar/specification.ML Isar/subclass.ML Isar/theory_target.ML Isar/toplevel.ML	\
-  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		\
+  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 Isar/locale.ML			\
+  Isar/method.ML Isar/net_rules.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/proof.ML Isar/proof_context.ML			\
+  Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML		\
+  Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML				\
+  Isar/spec_parse.ML Isar/specification.ML Isar/subclass.ML			\
+  Isar/theory_target.ML Isar/toplevel.ML 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		\
@@ -61,19 +62,21 @@
   ProofGeneral/pgml_isabelle.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 Tools/ROOT.ML Tools/invoke.ML 		\
-  Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML 		\
-  assumption.ML axclass.ML codegen.ML compress.ML config.ML conjunction.ML	\
-  consts.ML context.ML context_position.ML conv.ML defs.ML display.ML drule.ML	\
-  envir.ML fact_index.ML goal.ML interpretation.ML library.ML logic.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		\
+  Tools/ROOT.ML Tools/invoke.ML Tools/isabelle_process.ML			\
+  Tools/named_thms.ML Tools/xml_syntax.ML assumption.ML axclass.ML		\
+  codegen.ML compress.ML config.ML conjunction.ML consts.ML context.ML		\
+  context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML		\
+  fact_index.ML goal.ML interpretation.ML library.ML logic.ML			\
   meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML old_goals.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_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML variable.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_subst.ML theory.ML thm.ML type.ML			\
+  type_infer.ML unify.ML variable.ML
 	@./mk
 
 
diff -r b3e415b0cf5c -r 308315ee2b6d src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Thu Dec 20 21:09:38 2007 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Thu Dec 20 21:11:58 2007 +0100
@@ -35,6 +35,7 @@
 load "IO";
 
 use "ML-Systems/exn.ML";
+use "ML-Systems/universal.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
 
diff -r b3e415b0cf5c -r 308315ee2b6d src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Dec 20 21:09:38 2007 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Dec 20 21:11:58 2007 +0100
@@ -1,10 +1,12 @@
 (*  Title:      Pure/ML-Systems/polyml.ML
     ID:         $Id$
 
-Compatibility file for Poly/ML (version 4.1.3, 4.1.4 and 4.2.0).
+Compatibility file for Poly/ML (version 4.1.3, 4.1.4, 4.2.0, also shared by 5.x).
 *)
 
 use "ML-Systems/exn.ML";
+if List.exists (fn s => s = "Universal") (PolyML.Compiler.structureNames ()) then ()
+else use "ML-Systems/universal.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
 
@@ -194,7 +196,7 @@
 
 
 (*Convert a process ID to a decimal string (chiefly for tracing)*)
-fun string_of_pid pid = 
+fun string_of_pid pid =
   Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
 
 
diff -r b3e415b0cf5c -r 308315ee2b6d src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Dec 20 21:09:38 2007 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Dec 20 21:11:58 2007 +0100
@@ -7,6 +7,7 @@
 use "ML-Systems/proper_int.ML";
 use "ML-Systems/overloading_smlnj.ML";
 use "ML-Systems/exn.ML";
+use "ML-Systems/universal.ML";
 use "ML-Systems/multithreading.ML";