--- a/src/Tools/Code/code_runtime.ML Thu May 26 09:05:00 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML Thu May 26 15:27:50 2016 +0200
@@ -200,7 +200,7 @@
o reject_vars ctxt;
fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
- Code_Thingol.static_conv ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
+ Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
K (check_holds_oracle ctxt' (obtain_evaluator ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
end; (*local*)