| changeset 18392 | fdefc3cd45c5 |
| parent 18384 | fa38cca42913 |
| child 18760 | 97aaecb84afe |
| 18391:2e901da7cd3a | 18392:fdefc3cd45c5 |
|---|---|
22 fun install_pp _ = (); |
22 fun install_pp _ = (); |
23 |
23 |
24 fun print_depth _ = (); |
24 fun print_depth _ = (); |
25 |
25 |
26 fun exception_trace f = f (); |
26 fun exception_trace f = f (); |
27 fun print x = x; |
|
28 fun profile (n: int) f x = f x; |
27 fun profile (n: int) f x = f x; |
29 |
28 |
30 |
29 |
31 |
30 |
32 (** Basis structures **) |
31 (** Basis structures **) |