src/Pure/Isar/attrib.ML
changeset 36959 f5417836dbea
parent 36950 75b8f26f2f07
child 37198 3af985b10550
equal deleted inserted replaced
36958:ad5313f1bd30 36959:f5417836dbea
    45 end;
    45 end;
    46 
    46 
    47 structure Attrib: ATTRIB =
    47 structure Attrib: ATTRIB =
    48 struct
    48 struct
    49 
    49 
    50 structure T = OuterLex;
       
    51 
       
    52 
       
    53 (* source and bindings *)
    50 (* source and bindings *)
    54 
    51 
    55 type src = Args.src;
    52 type src = Args.src;
    56 
    53 
    57 type binding = binding * src list;
    54 type binding = binding * src list;
   214 
   211 
   215 (** basic attributes **)
   212 (** basic attributes **)
   216 
   213 
   217 (* internal *)
   214 (* internal *)
   218 
   215 
   219 fun internal att = Args.src (("Pure.attribute", [T.mk_attribute att]), Position.none);
   216 fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
   220 
   217 
   221 
   218 
   222 (* rule composition *)
   219 (* rule composition *)
   223 
   220 
   224 val COMP_att =
   221 val COMP_att =