src/Pure/ML/ml_compiler.ML
changeset 63806 c54a53ef1873
parent 62993 1de6405023a3
child 64660 ef85bb6491b3
--- a/src/Pure/ML/ml_compiler.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Mon Sep 05 23:11:00 2016 +0200
@@ -44,7 +44,7 @@
     | SOME 1 => pos
     | SOME j =>
         Position.properties_of pos
-        |> Properties.put (Markup.offsetN, Markup.print_int (j - 1))
+        |> Properties.put (Markup.offsetN, Value.print_int (j - 1))
         |> Position.of_properties)
   end;
 
@@ -89,7 +89,7 @@
         is_reported pos ?
           let
             fun markup () =
-              (Markup.entityN, [(if def then Markup.defN else Markup.refN, Markup.print_int id)]);
+              (Markup.entityN, [(if def then Markup.defN else Markup.refN, Value.print_int id)]);
           in cons (pos, markup, fn () => "") end
       end;