src/Tools/subtyping.ML
changeset 67149 e61557884799
parent 59936 b8ffc3dc9e24
     1.1 --- a/src/Tools/subtyping.ML	Wed Dec 06 19:34:59 2017 +0100
     1.2 +++ b/src/Tools/subtyping.ML	Wed Dec 06 20:43:09 2017 +0100
     1.3 @@ -882,7 +882,7 @@
     1.4  
     1.5  (* term check *)
     1.6  
     1.7 -val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false);
     1.8 +val coercion_enabled = Attrib.setup_config_bool \<^binding>\<open>coercion_enabled\<close> (K false);
     1.9  
    1.10  val _ =
    1.11    Theory.setup
    1.12 @@ -1097,16 +1097,16 @@
    1.13  
    1.14  val _ =
    1.15    Theory.setup
    1.16 -   (Attrib.setup @{binding coercion}
    1.17 +   (Attrib.setup \<^binding>\<open>coercion\<close>
    1.18        (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))
    1.19        "declaration of new coercions" #>
    1.20 -    Attrib.setup @{binding coercion_delete}
    1.21 +    Attrib.setup \<^binding>\<open>coercion_delete\<close>
    1.22        (Args.term >> (fn t => Thm.declaration_attribute (K (delete_coercion t))))
    1.23        "deletion of coercions" #>
    1.24 -    Attrib.setup @{binding coercion_map}
    1.25 +    Attrib.setup \<^binding>\<open>coercion_map\<close>
    1.26        (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
    1.27        "declaration of new map functions" #>
    1.28 -    Attrib.setup @{binding coercion_args}
    1.29 +    Attrib.setup \<^binding>\<open>coercion_args\<close>
    1.30        (Args.const {proper = false, strict = false} -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
    1.31          (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
    1.32        "declaration of new constants with coercion-invariant arguments");
    1.33 @@ -1115,7 +1115,7 @@
    1.34  (* outer syntax commands *)
    1.35  
    1.36  val _ =
    1.37 -  Outer_Syntax.command @{command_keyword print_coercions}
    1.38 +  Outer_Syntax.command \<^command_keyword>\<open>print_coercions\<close>
    1.39      "print information about coercions"
    1.40      (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)));
    1.41