src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML
changeset 62495 83db706d7771
parent 62494 b90109b2487c
child 62902 3c0f53eae166
equal deleted inserted replaced
62494:b90109b2487c 62495:83db706d7771
   182                 "",
   182                 "",
   183                 "end;"]
   183                 "end;"]
   184 
   184 
   185     in
   185     in
   186         compiled_rewriter := NONE;      
   186         compiled_rewriter := NONE;      
   187         ML_Compiler0.use_text ML_Env.local_context
   187         ML_Compiler0.use_text ML_Env.context
   188           {line = 1, file = "", verbose = false, debug = false} (!buffer);
   188           {line = 1, file = "", verbose = false, debug = false} (!buffer);
   189         case !compiled_rewriter of 
   189         case !compiled_rewriter of 
   190             NONE => raise (Compile "cannot communicate with compiled function")
   190             NONE => raise (Compile "cannot communicate with compiled function")
   191           | SOME r => (compiled_rewriter := NONE; r)
   191           | SOME r => (compiled_rewriter := NONE; r)
   192     end 
   192     end