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;