Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
afford strict Args.type_name (cf. 29e88714ffe4);
authorwenzelm
Fri, 16 Mar 2012 21:59:19 +0100
changeset 46971 bdec4a6016c2
parent 46970 9667e0dcb5e2
child 46972 ef6fc1a0884d
afford strict Args.type_name (cf. 29e88714ffe4);
src/HOL/Tools/Quotient/quotient_info.ML file | annotate | diff | comparison | revisions 
--- 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))
isabelle