| changeset 16660 | 76613dff2c9a |
| parent 16542 | 1259088dc448 |
| child 16681 | d54dfd724b35 |
--- a/src/Pure/ML-Systems/smlnj.ML Fri Jul 01 14:42:03 2005 +0200 +++ b/src/Pure/ML-Systems/smlnj.ML Fri Jul 01 14:42:04 2005 +0200 @@ -59,8 +59,10 @@ | _ => use "ML-Systems/cpu-timer-gc.ML"); -(* prompts *) +(*profiling -- dummy implementation*) +fun profile (n: int) f x = f x; +(*prompts*) fun ml_prompts p1 p2 = (Compiler.Control.primaryPrompt := p1; Compiler.Control.secondaryPrompt := p2);