changeset 62495 | 83db706d7771 |
parent 62494 | b90109b2487c |
child 62902 | 3c0f53eae166 |
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML Tue Mar 01 22:11:36 2016 +0100 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML Tue Mar 01 22:49:33 2016 +0100 @@ -184,7 +184,7 @@ in compiled_rewriter := NONE; - ML_Compiler0.use_text ML_Env.local_context + ML_Compiler0.use_text ML_Env.context {line = 1, file = "", verbose = false, debug = false} (!buffer); case !compiled_rewriter of NONE => raise (Compile "cannot communicate with compiled function")