# HG changeset patch # User wenzelm # Date 1738006142 -3600 # Node ID 5e50a2b5280986e0e4fae43ec3d7bd2272537416 # Parent f62e7c3ab25400ced4144a04c05df6d5c2602896 support for "no" polarity of 'adhoc_overloading' vs. 'no_adhoc_overloading'; diff -r f62e7c3ab254 -r 5e50a2b52809 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Mon Jan 27 18:32:18 2025 +0100 +++ b/src/Doc/Isar_Ref/Spec.thy Mon Jan 27 20:29:02 2025 +0100 @@ -296,6 +296,7 @@ \<^item> @{command translations} versus @{command no_translations} \<^item> @{command notation} versus @{command no_notation} \<^item> @{command type_notation} versus @{command no_type_notation} + \<^item> @{command adhoc_overloading} versus @{command no_adhoc_overloading} This also works recursively for the @{command unbundle} command as declaration inside a @{command bundle} definition: \<^verbatim>\no\ means that diff -r f62e7c3ab254 -r 5e50a2b52809 src/Pure/Tools/adhoc_overloading.ML --- a/src/Pure/Tools/adhoc_overloading.ML Mon Jan 27 18:32:18 2025 +0100 +++ b/src/Pure/Tools/adhoc_overloading.ML Mon Jan 27 20:29:02 2025 +0100 @@ -203,14 +203,14 @@ local -fun generic_adhoc_overloading add = - if add then +fun generic_adhoc_overloading add args context = + if Syntax.effective_polarity_generic context add then fold (fn (oconst, ts) => generic_add_overloaded oconst - #> fold (generic_add_variant oconst) ts) + #> fold (generic_add_variant oconst) ts) args context else fold (fn (oconst, ts) => - fold (generic_remove_variant oconst) ts); + fold (generic_remove_variant oconst) ts) args context; fun gen_adhoc_overloading prep_arg add raw_args lthy = let