tuned signature;

--- a/src/Pure/General/symbol_pos.ML	Tue Mar 29 20:52:19 2016 +0200
+++ b/src/Pure/General/symbol_pos.ML	Tue Mar 29 20:53:52 2016 +0200
@@ -42,6 +42,7 @@
   val implode: T list -> text
   val implode_range: Position.range -> T list -> text * Position.range
   val explode: text * Position.T -> T list
+  val explode0: string -> T list
   val scan_ident: T list -> T list * T list
   val is_identifier: string -> bool
 end;
@@ -271,6 +272,8 @@
         (Symbol.explode str) ([], Position.reset_range pos);
   in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
 
+fun explode0 str = explode (str, Position.none);
+
 
 (* identifiers *)
 
@@ -289,7 +292,7 @@
 
 fun is_identifier s =
   Symbol.is_ascii_identifier s orelse
-    (case try (Scan.finite stopper scan_ident) (explode (s, Position.none)) of
+    (case try (Scan.finite stopper scan_ident) (explode0 s) of
       SOME (_, []) => true
     | _ => false);
 
@@ -302,4 +305,3 @@
   val $$$ = Symbol_Pos.$$$;
   val ~$$$ = Symbol_Pos.~$$$;
 end;
-

--- a/src/Pure/Syntax/lexicon.ML	Tue Mar 29 20:52:19 2016 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Mar 29 20:53:52 2016 +0200
@@ -327,7 +327,7 @@
 (* indexname *)
 
 fun read_indexname s =
-  (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode (s, Position.none)) of
+  (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode0 s) of
     SOME xi => xi
   | _ => error ("Lexical error in variable name: " ^ quote s));
 
@@ -341,14 +341,14 @@
         >> Syntax.var ||
       Scan.many (Symbol.not_eof o Symbol_Pos.symbol)
         >> (Syntax.free o implode o map Symbol_Pos.symbol);
-  in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
+  in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str)) end;
 
 
 (* read_variable *)
 
 fun read_variable str =
   let val scan = $$ "?" |-- scan_indexname || scan_indexname
-  in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
+  in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str) end;
 
 
 (* read numbers *)
@@ -361,10 +361,10 @@
 
 in
 
-fun read_nat s = nat (Symbol_Pos.explode (s, Position.none));
+fun read_nat s = nat (Symbol_Pos.explode0 s);
 
 fun read_int s =
-  (case Symbol_Pos.explode (s, Position.none) of
+  (case Symbol_Pos.explode0 s of
     ("-", _) :: cs => Option.map ~ (nat cs)
   | cs => nat cs);
 

--- a/src/Pure/Syntax/simple_syntax.ML	Tue Mar 29 20:52:19 2016 +0200
+++ b/src/Pure/Syntax/simple_syntax.ML	Tue Mar 29 20:53:52 2016 +0200
@@ -21,7 +21,7 @@
 
 fun read scan s =
   (case
-      Symbol_Pos.explode (s, Position.none) |>
+      Symbol_Pos.explode0 s |>
       Lexicon.tokenize lexicon false |>
       filter Lexicon.is_proper |>
       Scan.read Lexicon.stopper scan of