# HG changeset patch
# User wenzelm
# Date 1732981342 -3600
# Node ID 98cb63b447c6814efafa21d42b31db610e9bb6aa
# Parent  d11ed1bf0ad2e28d3a2cb11845c0e1e25b2e4d88
clarified 'unbundle' polarity, according to algebraic group laws;

diff -r d11ed1bf0ad2 -r 98cb63b447c6 NEWS
--- a/NEWS	Sat Nov 30 16:01:58 2024 +0100
+++ b/NEWS	Sat Nov 30 16:42:22 2024 +0100
@@ -81,12 +81,12 @@
 
 * Command "unbundle b" and its variants like "context includes b" allow
 an optional name prefix with the reserved word "no": "unbundle no b"
-etc. This inverts the polarity of bundled declarations like 'notation'
-vs. 'no_notation', and thus avoids redundant bundle definitions like
-"foobar_syntax" vs. "no_foobar_syntax", because "no foobar_syntax" may
-be used instead. Consequently, the syntax for multiple bundle names has
-been changed slightly, demanding an explicit 'and' keyword. Minor
-INCOMPATIBILITY.
+etc. This reverses both the order and polarity of bundled declarations
+like 'notation' vs. 'no_notation', and thus avoids redundant bundle
+definitions like "foobar_syntax" vs. "no_foobar_syntax", because "no
+foobar_syntax" may be used instead. Consequently, the syntax for
+multiple bundle names has been changed slightly, demanding an explicit
+'and' keyword. Minor INCOMPATIBILITY.
 
 * Command "open_bundle b" is like "bundle b" followed by "unbundle b",
 so its declarations are applied immediately, but also named for later
diff -r d11ed1bf0ad2 -r 98cb63b447c6 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Sat Nov 30 16:01:58 2024 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Nov 30 16:42:22 2024 +0100
@@ -297,7 +297,9 @@
     \<^item> @{command type_notation} versus @{command no_type_notation}
 
   This also works recursively for the @{command unbundle} command as
-  declaration inside a @{command bundle} definition.
+  declaration inside a @{command bundle} definition: \<^verbatim>\<open>no\<close> means that
+  both the order and polarity of declarations is reversed (following
+  algebraic group laws).
 
 
   Here is an artificial example of bundling various configuration options:
diff -r d11ed1bf0ad2 -r 98cb63b447c6 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sat Nov 30 16:01:58 2024 +0100
+++ b/src/Pure/Isar/bundle.ML	Sat Nov 30 16:42:22 2024 +0100
@@ -126,10 +126,11 @@
     val notes = if loc then Local_Theory.notes else Attrib.local_notes "";
     val add0 = Syntax.get_polarity ctxt;
     val add1 = Syntax.effective_polarity ctxt add;
+    val bundle' = if add1 then bundle else rev (map (apsnd rev) bundle);
   in
     ctxt
     |> Context_Position.set_visible false
-    |> notes [(Binding.empty_atts, polarity_decls add1 @ bundle @ polarity_decls add0)] |> snd
+    |> notes [(Binding.empty_atts, polarity_decls add1 @ bundle' @ polarity_decls add0)] |> snd
     |> Context_Position.restore_visible ctxt
   end;