| changeset 31321 | fe786d4633b9 |
| parent 30672 | beaadd5af500 |
| child 31427 | 5a07cc86675d |
| 31320:72eeb1b4e006 | 31321:fe786d4633b9 |
|---|---|
130 fun profile (n: int) f x = f x; |
130 fun profile (n: int) f x = f x; |
131 |
131 |
132 (*dummy implementation*) |
132 (*dummy implementation*) |
133 fun exception_trace f = f (); |
133 fun exception_trace f = f (); |
134 |
134 |
135 (*dummy implementation*) |
|
136 fun print x = x; |
|
137 |
135 |
138 |
136 |
139 (** Compiler-independent timing functions **) |
137 (** Compiler-independent timing functions **) |
140 |
138 |
141 load "Timer"; |
139 load "Timer"; |