src/Pure/Isar/attrib.ML
changeset 61819 7e020220561a
parent 61816 93d0af296c2f
child 61851 ccf2df82b2d3
equal deleted inserted replaced
61818:6de8e7ad95c3 61819:7e020220561a
   240 
   240 
   241 (* internal attribute *)
   241 (* internal attribute *)
   242 
   242 
   243 fun internal att =
   243 fun internal att =
   244   Token.make_src ("Pure.attribute", Position.none)
   244   Token.make_src ("Pure.attribute", Position.none)
   245     [Token.make_value "<attribute>" (Token.Attribute att)];
   245     [Token.make_string ("<attribute>", Position.none) |> Token.assign (SOME (Token.Attribute att))];
   246 
   246 
   247 val _ = Theory.setup
   247 val _ = Theory.setup
   248   (setup (Binding.make ("attribute", @{here}))
   248   (setup (Binding.make ("attribute", @{here}))
   249     (Scan.lift Args.internal_attribute >> Morphism.form)
   249     (Scan.lift Args.internal_attribute >> Morphism.form)
   250     "internal attribute");
   250     "internal attribute");