diff -r c272680df665 -r c54a53ef1873 src/Pure/ML/ml_compiler.ML --- 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;