1.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 16 21:40:21 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 16 21:59:19 2012 +0100
     1.3 @@ -71,8 +71,7 @@
     1.4  
     1.5  val quotmaps_attribute_setup =
     1.6    Attrib.setup @{binding map}
     1.7 -    ((Args.type_name false --| Scan.lift (@{keyword "="})) --  (* FIXME Args.type_name true (requires "set" type) *)
     1.8 -      Args.const_proper true >>
     1.9 +    ((Args.type_name true --| Scan.lift (@{keyword "="})) -- Args.const_proper true >>
    1.10        (fn (tyname, relname) =>
    1.11          let val minfo = {relmap = relname}
    1.12          in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))