--- a/src/Tools/Compute_Oracle/am_compiler.ML Mon Mar 23 22:38:02 2009 +0100
+++ b/src/Tools/Compute_Oracle/am_compiler.ML Mon Mar 23 22:56:03 2009 +0100
@@ -185,7 +185,7 @@
in
compiled_rewriter := NONE;
- use_text ML_Context.name_space (1, "") Output.ml_output false (!buffer);
+ use_text ML_Context.local_context (1, "") false (!buffer);
case !compiled_rewriter of
NONE => raise (Compile "cannot communicate with compiled function")
| SOME r => (compiled_rewriter := NONE; r)
--- a/src/Tools/Compute_Oracle/am_sml.ML Mon Mar 23 22:38:02 2009 +0100
+++ b/src/Tools/Compute_Oracle/am_sml.ML Mon Mar 23 22:56:03 2009 +0100
@@ -492,7 +492,7 @@
fun writeTextFile name s = File.write (Path.explode name) s
-fun use_source src = use_text ML_Context.name_space (1, "") Output.ml_output false src
+fun use_source src = use_text ML_Context.local_context (1, "") false src
fun compile cache_patterns const_arity eqs =
let