src/Pure/ML/ml_compiler_polyml.ML

   let
     val {file = text, startLine = line, startPosition = offset,
       endLine = _, endPosition = end_offset} = loc;
     val props =
       (case YXML.parse text of
-        XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else []
+        XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
       | XML.Text s => Position.file_name s);
   in
     Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
   end;
 

         SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
       | _ => Position.reported_text);
 
     fun reported_entity kind loc decl =
       reported_text (position_of loc)
-        (Isabelle_Markup.entityN,
-          (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
+        (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
 
     fun reported loc (PolyML.PTtype types) =
           cons
             (PolyML.NameSpace.displayTypeExpression (types, depth, space)
               |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
-              |> reported_text (position_of loc) Isabelle_Markup.ML_typing)
+              |> reported_text (position_of loc) Markup.ML_typing)
       | reported loc (PolyML.PTdeclaredAt decl) =
-          cons (reported_entity Isabelle_Markup.ML_defN loc decl)
+          cons (reported_entity Markup.ML_defN loc decl)
       | reported loc (PolyML.PTopenedAt decl) =
-          cons (reported_entity Isabelle_Markup.ML_openN loc decl)
+          cons (reported_entity Markup.ML_openN loc decl)
       | reported loc (PolyML.PTstructureAt decl) =
-          cons (reported_entity Isabelle_Markup.ML_structN loc decl)
+          cons (reported_entity Markup.ML_structN loc decl)
       | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
       | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
       | reported _ _ = I
     and reported_tree (loc, props) = fold (reported loc) props;
   in fn tree => Output.report (implode (reported_tree tree [])) end;

 
 
     (* input *)
 
     val location_props =
-      op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties
-            (filter (member (op =)
-              [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos))));
+      op ^
+        (YXML.output_markup (Markup.position |> Markup.properties
+          (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))));
 
     val input_buffer =
       Unsynchronized.ref (toks |> map
         (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of)));