changeset 32740 | 9dd0a2f83429 |
parent 30970 | 3fe2e418a071 |
child 34028 | 1e6206763036 |
32739:31e75ad9ae17 | 32740:9dd0a2f83429 |
---|---|
46 |
46 |
47 ML {* |
47 ML {* |
48 structure Eval_Witness_Method = |
48 structure Eval_Witness_Method = |
49 struct |
49 struct |
50 |
50 |
51 val eval_ref : (unit -> bool) option ref = ref NONE; |
51 val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE; |
52 |
52 |
53 end; |
53 end; |
54 *} |
54 *} |
55 |
55 |
56 oracle eval_witness_oracle = {* fn (cgoal, ws) => |
56 oracle eval_witness_oracle = {* fn (cgoal, ws) => |