| changeset 21295 | 63552bc99cfb |
| parent 18760 | 97aaecb84afe |
| child 21770 | ea6f846d8c4b |
--- a/src/Pure/ML-Systems/poplogml.ML Fri Nov 10 22:18:54 2006 +0100 +++ b/src/Pure/ML-Systems/poplogml.ML Fri Nov 10 23:22:01 2006 +0100 @@ -247,9 +247,9 @@ (** Compiler-independent timing functions **) -fun startTiming() = "FIXME"; -fun endTiming (s: string) = s; -fun checkTimer _ = (0, 0, 0); +fun start_timing() = "FIXME"; +fun end_timing (s: string) = s; +fun check_timer _ = (0, 0, 0); structure Timer = struct