src/Pure/ProofGeneral/proof_general_pgip.ML

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 25 19:49:24 2012 +0100
@@ -101,8 +101,7 @@
 val pgml_syms = map pgml_sym o Symbol.explode;
 
 val token_markups =
- [Isabelle_Markup.tfreeN, Isabelle_Markup.tvarN, Isabelle_Markup.freeN,
-  Isabelle_Markup.boundN, Isabelle_Markup.varN, Isabelle_Markup.skolemN];
+  [Markup.tfreeN, Markup.tvarN, Markup.freeN, Markup.boundN, Markup.varN, Markup.skolemN];
 
 fun get_int props name =
   (case Properties.get props name of NONE => NONE | SOME s => Int.fromString s);
@@ -115,11 +114,10 @@
         in [Pgml.Atoms {kind = SOME name, content = content}] end
       else
         let val content = maps pgml_terms body in
-          if name = Isabelle_Markup.blockN then
-            [Pgml.Box {orient = NONE,
-              indent = get_int atts Isabelle_Markup.indentN, content = content}]
-          else if name = Isabelle_Markup.breakN then
-            [Pgml.Break {mandatory = NONE, indent = get_int atts Isabelle_Markup.widthN}]
+          if name = Markup.blockN then
+            [Pgml.Box {orient = NONE, indent = get_int atts Markup.indentN, content = content}]
+          else if name = Markup.breakN then
+            [Pgml.Break {mandatory = NONE, indent = get_int atts Markup.widthN}]
           else content
         end
   | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
@@ -138,7 +136,7 @@
     val area =
       (case body of
         [XML.Elem ((name, _), _)] =>
-          if name = Isabelle_Markup.stateN then PgipTypes.Display else default_area
+          if name = Markup.stateN then PgipTypes.Display else default_area
       | _ => default_area);
   in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;