src/Pure/Isar/attrib.ML
changeset 58865 ce8d13995516
parent 58047 9f3826352b52
child 58903 38c72f5f6c2e
--- 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;