# HG changeset patch
# User wenzelm
# Date 1414867668 -3600
# Node ID ce8d13995516fe6c7f0620827a70f09df7e3ae89
# Parent  505a8150368a86a5b586aca02255f778378aca58
tuned signature (see ab2483fad861);

diff -r 505a8150368a -r ce8d13995516 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Nov 01 19:33:51 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Sat Nov 01 19:47:48 2014 +0100
@@ -291,7 +291,7 @@
     val syms = Symbol_Pos.source_explode source;
     val lex = #1 (Keyword.get_lexicons ());
   in
-    (case Token.read lex Parse.attribs (syms, #pos source) of
+    (case Token.read lex Parse.attribs syms of
       [raw_srcs] => check_attribs ctxt raw_srcs
     | _ => error ("Malformed attributes" ^ Position.here (#pos source)))
   end;
diff -r 505a8150368a -r ce8d13995516 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sat Nov 01 19:33:51 2014 +0100
+++ b/src/Pure/Isar/token.ML	Sat Nov 01 19:47:48 2014 +0100
@@ -87,7 +87,7 @@
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   type 'a parser = T list -> 'a * T list
   type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
-  val read: Scan.lexicon -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a list
+  val read: Scan.lexicon -> 'a parser -> Symbol_Pos.T list -> 'a list
   val read_antiq: Scan.lexicon -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
@@ -582,7 +582,7 @@
 
 (* read source *)
 
-fun read lex scan (syms, pos) =
+fun read lex scan syms =
   Source.of_list syms
   |> source' true (K (lex, Scan.empty_lexicon))
   |> source_proper
@@ -594,7 +594,7 @@
     fun err msg =
       cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
         "@{" ^ Symbol_Pos.content syms ^ "}");
-    val res = read lex scan (syms, pos) handle ERROR msg => err msg;
+    val res = read lex scan syms handle ERROR msg => err msg;
   in (case res of [x] => x | _ => err "") end;