# HG changeset patch
# User wenzelm
# Date 1331931559 -3600
# Node ID bdec4a6016c269c1f0cd710112a15abfa9fe838a
# Parent  9667e0dcb5e24ec17524508e34e97699ba4f6733
afford strict Args.type_name (cf. 29e88714ffe4);

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