# 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>\<open>no\<close> 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