src/Pure/Tools/codegen_serializer.ML
changeset 20926 b2f67b947200
parent 20896 1484c7af6d68
child 20931 19d9b78218fd
--- a/src/Pure/Tools/codegen_serializer.ML	Mon Oct 09 19:37:04 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Mon Oct 09 19:37:05 2006 +0200
@@ -1123,7 +1123,7 @@
 fun parse_internal serializer =
   parse_args (Args.name
   >> (fn "-" => serializer
-        (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE))
+        (fn "" => (fn p => (use_text Output.ml_output false (Pretty.output p); NONE))
           | _ => SOME)
        | _ => Scan.fail ()));
 
@@ -1241,13 +1241,13 @@
       else Pretty.output p;
     val serializer = ml_serializer struct_name "SML" [[nsp_module], [nsp_class, nsp_tyco],
       [nsp_fun, nsp_dtco, nsp_class, nsp_classop, nsp_inst], [nsp_eval]]
-      (fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (output p); NONE))
+      (fn "" => (fn p => (use_text Output.ml_output (!eval_verbose) (output p); NONE))
         | _ => SOME) data
         (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]);
     val _ = serializer code';
     val val_name_struct = NameSpace.append struct_name val_name;
     val _ = reff := NONE;
-    val _ = use_text Context.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name_struct ^ "))");
+    val _ = use_text Output.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name_struct ^ "))");
   in case !reff
    of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
         ^ " (reference probably has been shadowed)")