equal
deleted
inserted
replaced
31 *} |
31 *} |
32 |
32 |
33 oracle mc_eindhoven_oracle ("term") = |
33 oracle mc_eindhoven_oracle ("term") = |
34 {* |
34 {* |
35 let |
35 let |
36 val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Sign.string_of_term; |
36 val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global; |
37 |
37 |
38 fun call_mc s = |
38 fun call_mc s = |
39 let |
39 let |
40 val eindhoven_home = getenv "EINDHOVEN_HOME"; |
40 val eindhoven_home = getenv "EINDHOVEN_HOME"; |
41 val pmu = |
41 val pmu = |