tuned;
authorwenzelm
Tue Sep 20 14:03:40 2005 +0200 (2005-09-20 ago)
changeset 1751151314f4bd01d
parent 17510 5e3ce025e1a5
child 17512 854d061f6c10
tuned;
src/Pure/Isar/context_rules.ML
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/Pure/Isar/context_rules.ML	Tue Sep 20 14:03:39 2005 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Tue Sep 20 14:03:40 2005 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4  
     1.5  structure GlobalRulesArgs =
     1.6  struct
     1.7 -  val name = "Isar/rule_context";
     1.8 +  val name = "Isar/rules";
     1.9    type T = T;
    1.10  
    1.11    val empty = make_rules ~1 [] empty_netpairs ([], []);
     2.1 --- a/src/Pure/ML-Systems/smlnj.ML	Tue Sep 20 14:03:39 2005 +0200
     2.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Tue Sep 20 14:03:40 2005 +0200
     2.3 @@ -63,10 +63,10 @@
     2.4  fun ml_prompts p1 p2 =
     2.5    (Compiler.Control.primaryPrompt := p1; Compiler.Control.secondaryPrompt := p2);
     2.6  
     2.7 -(*dummy impelemtation*)
     2.8 +(*dummy implementation*)
     2.9  fun profile (n: int) f x = f x;
    2.10  
    2.11 -(*dummy impelemtation*)
    2.12 +(*dummy implementation*)
    2.13  fun exception_trace f = f ();
    2.14  
    2.15  (case #version_id (Compiler.version) of
    2.16 @@ -143,6 +143,7 @@
    2.17  
    2.18  end;
    2.19  
    2.20 +
    2.21  (** Signal handling: emulation of the Poly/ML Signal structure. Note that types
    2.22      Posix.Signal.signal and Signals.signal differ **)
    2.23