src/Pure/Isar/proof_context.ML

 (* classes *)
 
 fun read_class ctxt text =
   let
     val tsig = tsig_of ctxt;
-    val {text, pos, ...} = Syntax.read_token_source text;
-    val syms = Symbol_Pos.explode (text, pos);
-    val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
+    val (s, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+    val c = Type.cert_class tsig (Type.intern_class tsig s)
       handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
     val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
   in c end;
 
 

 in
 
 fun read_type_name ctxt strict text =
   let
     val tsig = tsig_of ctxt;
-    val (c, pos) = Syntax.read_token_content text;
+    val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
   in
     if Lexicon.is_tid c then
      (Context_Position.report ctxt pos Markup.tfree;
       TFree (c, default_sort ctxt (c, ~1)))
     else

     T as Type _ => T
   | T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
 
 
 fun read_const_proper ctxt strict =
-  prep_const_proper ctxt strict o Syntax.read_token_content;
+  prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;
 
 fun read_const ctxt strict ty text =
   let
-    val (c, pos) = Syntax.read_token_content text;
+    val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
     val _ = no_skolem false c;
   in
     (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
       (SOME x, false) =>
         (Context_Position.report ctxt pos