--- a/src/Pure/Isar/attrib.ML Wed Oct 31 15:50:45 2018 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Oct 31 15:53:32 2018 +0100
@@ -214,12 +214,11 @@
fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
-fun attribute_setup (name, pos) source comment =
- ML_Lex.read_source source
- |> ML_Context.expression ("parser", pos) "Thm.attribute context_parser"
- ("Context.map_proof (Attrib.local_setup " ^
- ML_Syntax.atomic (ML_Syntax.make_binding (name, pos)) ^
- " parser " ^ ML_Syntax.print_string comment ^ ")")
+fun attribute_setup binding source comment =
+ ML_Context.expression (Input.pos_of source)
+ (ML_Lex.read
+ ("Theory.local_setup (Attrib.local_setup (" ^ ML_Syntax.make_binding binding ^ ") (") @
+ ML_Lex.read_source source @ ML_Lex.read (") " ^ ML_Syntax.print_string comment ^ ")"))
|> Context.proof_map;