src/Pure/PIDE/command.ML

       if null verbatim then ()
       else legacy_feature ("Old-style {* verbatim *} token -- use \<open>cartouche\<close> instead" ^
         Position.here_list verbatim);
   in
     if exists #1 token_reports
-    then Toplevel.malformed (Token.core_range_of span) "Malformed command syntax"
+    then Toplevel.malformed (#1 (Token.core_range_of span)) "Malformed command syntax"
     else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span)
   end;
 
 end;