# HG changeset patch
# User wenzelm
# Date 1515332934 -3600
# Node ID fbc31dea36fac54d436e4305ad3b5420b00f6331
# Parent  fed0e220be45f6884fa48adcf130c397aebfa0e6
tuned;

diff -r fed0e220be45 -r fbc31dea36fa src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Jan 07 14:39:56 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Jan 07 14:48:54 2018 +0100
@@ -314,7 +314,7 @@
 (* presentation tokens *)
 
 datatype token =
-    No_Token
+    Ignore_Token
   | Basic_Token of Token.T
   | Markup_Token of string * Input.source
   | Markup_Env_Token of string * Input.source
@@ -330,7 +330,7 @@
 
 fun present_token state tok =
   (case tok of
-    No_Token => []
+    Ignore_Token => []
   | Basic_Token tok => output_token state tok
   | Markup_Token (cmd, source) =>
       Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
@@ -484,7 +484,7 @@
     (* tokens *)
 
     val ignored = Scan.state --| ignore
-      >> (fn d => (NONE, (No_Token, ("", d))));
+      >> (fn d => (NONE, (Ignore_Token, ("", d))));
 
     fun markup pred mk flag = Scan.peek (fn d =>
       improper |--