equal
deleted
inserted
replaced
709 |
709 |
710 (** installation **) |
710 (** installation **) |
711 |
711 |
712 (* term check *) |
712 (* term check *) |
713 |
713 |
714 val (coercion_enabled, coercion_enabled_setup) = |
714 val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false); |
715 Attrib.config_bool "coercion_enabled" (K false); |
|
716 |
715 |
717 val add_term_check = |
716 val add_term_check = |
718 Syntax.add_term_check ~100 "coercions" |
717 Syntax.add_term_check ~100 "coercions" |
719 (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt); |
718 (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt); |
720 |
719 |
818 |
817 |
819 |
818 |
820 (* theory setup *) |
819 (* theory setup *) |
821 |
820 |
822 val setup = |
821 val setup = |
823 coercion_enabled_setup #> |
|
824 Context.theory_map add_term_check #> |
822 Context.theory_map add_term_check #> |
825 Attrib.setup @{binding coercion} |
823 Attrib.setup @{binding coercion} |
826 (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t)))) |
824 (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t)))) |
827 "declaration of new coercions" #> |
825 "declaration of new coercions" #> |
828 Attrib.setup @{binding coercion_map} |
826 Attrib.setup @{binding coercion_map} |