Quot/quotient_typ.ML
changeset 1155 5650924c69ed
parent 1152 fbaebf08c1bd
child 1162 6642df770bc4
equal deleted inserted replaced
1152:fbaebf08c1bd 1155:5650924c69ed
   293 local
   293 local
   294   structure P = OuterParse;
   294   structure P = OuterParse;
   295 in
   295 in
   296 
   296 
   297 val quotspec_parser =
   297 val quotspec_parser =
   298     P.and_list1 ((P.type_args -- P.binding) -- P.opt_infix -- 
   298   P.and_list1 ((P.type_args -- P.binding) -- P.opt_infix -- 
   299        (P.$$$ "=" |-- P.typ) -- (P.$$$ "/" |-- P.term))
   299     (P.$$$ "=" |-- P.typ) -- (P.$$$ "/" |-- P.term))
   300 end
   300 end
   301 
   301 
   302 val _ = OuterKeyword.keyword "/"
   302 val _ = OuterKeyword.keyword "/"
   303 
   303 
   304 val _ =
   304 val _ =