diff -r dd154240a53c -r b90109b2487c src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Tue Mar 01 21:10:29 2016 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Tue Mar 01 22:11:36 2016 +0100
@@ -184,7 +184,7 @@
 
     in
         compiled_rewriter := NONE;      
-        use_text ML_Env.local_context
+        ML_Compiler0.use_text ML_Env.local_context
           {line = 1, file = "", verbose = false, debug = false} (!buffer);
         case !compiled_rewriter of 
             NONE => raise (Compile "cannot communicate with compiled function")