src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML
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")