diff -r c7ba9b133bd4 -r a7f6359665c6 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Apr 02 20:07:05 2015 +0200
+++ b/src/Pure/Isar/token.ML	Thu Apr 02 20:07:32 2015 +0200
@@ -32,6 +32,7 @@
   val pos_of: T -> Position.T
   val range_of: T list -> Position.range
   val src: xstring * Position.T -> T list -> src
+  val src_checked: string * Position.T -> T list -> string * Markup.T -> src
   val name_of_src: src -> string * Position.T
   val args_of_src: src -> T list
   val range_of_src: src -> Position.T
@@ -161,7 +162,7 @@
   Src of
    {name: string * Position.T,
     args: T list,
-    checked_markup: (string * Markup.T) option}
+    checked: (string * Markup.T) option}
 
 and slot =
   Slot |
@@ -195,10 +196,11 @@
 
 (* src *)
 
-fun src name args = Src {name = name, args = args, checked_markup = NONE};
+fun src name args = Src {name = name, args = args, checked = NONE};
+fun src_checked name args checked = Src {name = name, args = args, checked = SOME checked};
 
-fun map_args f (Src {name, args, checked_markup}) =
-  Src {name = name, args = map f args, checked_markup = checked_markup};
+fun map_args f (Src {name, args, checked}) =
+  Src {name = name, args = map f args, checked = checked};
 
 fun name_of_src (Src {name, ...}) = name;
 fun args_of_src (Src {args, ...}) = args;
@@ -207,15 +209,15 @@
   if null args then pos
   else Position.set_range (pos, #2 (range_of args));
 
-fun check_src _ table (src as Src {name = (name, _), checked_markup = SOME _, ...}) =
+fun check_src _ table (src as Src {name = (name, _), checked = SOME _, ...}) =
       (src, Name_Space.get table name)
-  | check_src ctxt table (Src {name = (xname, pos), args, checked_markup = NONE}) =
+  | check_src ctxt table (Src {name = (xname, pos), args, checked = NONE}) =
       let
         val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
         val space = Name_Space.space_of_table table;
         val kind = Name_Space.kind_of space;
         val markup = Name_Space.markup space name;
-      in (Src {name = (name, pos), args = args, checked_markup = SOME (kind, markup)}, x) end;
+      in (src_checked (name, pos) args (kind, markup), x) end;
 
 
 (* stopper *)
@@ -478,9 +480,9 @@
 
 fun pretty_src ctxt src =
   let
-    val Src {name = (name, _), args, checked_markup} = src;
+    val Src {name = (name, _), args, checked} = src;
     val prt_name =
-      (case checked_markup of
+      (case checked of
         NONE => Pretty.str name
       | SOME (_, markup) => Pretty.mark_str (markup, name));
     val prt_arg = pretty_value ctxt;
@@ -663,7 +665,7 @@
 
 (* wrapped syntax *)
 
-fun syntax_generic scan (Src {name = (name, pos), args = args0, checked_markup}) context =
+fun syntax_generic scan (Src {name = (name, pos), args = args0, checked}) context =
   let
     val args1 = map init_assignable args0;
     fun reported_text () =
@@ -679,7 +681,7 @@
     | (_, (_, args2)) =>
         let
           val print_name =
-            (case checked_markup of
+            (case checked of
               NONE => quote name
             | SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name));
           val print_args =
@@ -696,4 +698,3 @@
 
 type 'a parser = 'a Token.parser;
 type 'a context_parser = 'a Token.context_parser;
-