diff -r 51890cb80b30 -r 92b6f4e68c5a src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue Nov 11 21:14:19 2014 +0100 +++ b/src/Pure/Isar/attrib.ML Wed Nov 12 10:30:59 2014 +0100 @@ -208,8 +208,7 @@ fun attribute_setup name source comment = ML_Lex.read_source false source - |> ML_Context.expression (#range source) - "val parser: Thm.attribute context_parser" + |> ML_Context.expression (#range source) "parser" "Thm.attribute context_parser" ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^ " parser " ^ ML_Syntax.print_string comment ^ ")") |> Context.proof_map;