| changeset 32740 | 9dd0a2f83429 |
| parent 32603 | e08fdd615333 |
| child 32966 | 5b21661fe618 |
| 32739:31e75ad9ae17 | 32740:9dd0a2f83429 |
|---|---|
9 struct |
9 struct |
10 |
10 |
11 local open FundefLib in |
11 local open FundefLib in |
12 |
12 |
13 (* Profiling *) |
13 (* Profiling *) |
14 val profile = ref false; |
14 val profile = Unsynchronized.ref false; |
15 |
15 |
16 fun PROFILE msg = if !profile then timeap_msg msg else I |
16 fun PROFILE msg = if !profile then timeap_msg msg else I |
17 |
17 |
18 |
18 |
19 val acc_const_name = @{const_name accp} |
19 val acc_const_name = @{const_name accp} |