# HG changeset patch # User wenzelm # Date 1127217820 -7200 # Node ID 51314f4bd01daacd20322c2675c48feb0a584901 # Parent 5e3ce025e1a5eb154ab08250c88a5b4d9603161b tuned; diff -r 5e3ce025e1a5 -r 51314f4bd01d src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Tue Sep 20 14:03:39 2005 +0200 +++ b/src/Pure/Isar/context_rules.ML Tue Sep 20 14:03:40 2005 +0200 @@ -121,7 +121,7 @@ structure GlobalRulesArgs = struct - val name = "Isar/rule_context"; + val name = "Isar/rules"; type T = T; val empty = make_rules ~1 [] empty_netpairs ([], []); diff -r 5e3ce025e1a5 -r 51314f4bd01d src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Tue Sep 20 14:03:39 2005 +0200 +++ b/src/Pure/ML-Systems/smlnj.ML Tue Sep 20 14:03:40 2005 +0200 @@ -63,10 +63,10 @@ fun ml_prompts p1 p2 = (Compiler.Control.primaryPrompt := p1; Compiler.Control.secondaryPrompt := p2); -(*dummy impelemtation*) +(*dummy implementation*) fun profile (n: int) f x = f x; -(*dummy impelemtation*) +(*dummy implementation*) fun exception_trace f = f (); (case #version_id (Compiler.version) of @@ -143,6 +143,7 @@ end; + (** Signal handling: emulation of the Poly/ML Signal structure. Note that types Posix.Signal.signal and Signals.signal differ **)