src/Tools/subtyping.ML
changeset 55954 a29aefc88c8d
parent 55763 4b3907cb5654
child 56334 6b3739fee456
     1.1 --- a/src/Tools/subtyping.ML	Thu Mar 06 12:58:51 2014 +0100
     1.2 +++ b/src/Tools/subtyping.ML	Thu Mar 06 13:44:01 2014 +0100
     1.3 @@ -1105,7 +1105,7 @@
     1.4      (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
     1.5      "declaration of new map functions" #>
     1.6    Attrib.setup @{binding coercion_args}
     1.7 -    (Args.const false -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
     1.8 +    (Args.const {proper = false, strict = false} -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
     1.9        (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
    1.10      "declaration of new constants with coercion-invariant arguments";
    1.11