# HG changeset patch
# User wenzelm
# Date 1737999138 -3600
# Node ID f62e7c3ab25400ced4144a04c05df6d5c2602896
# Parent  be1328008ee2efe0c4c05334e9679efec4ffbc5e
more operations;

diff -r be1328008ee2 -r f62e7c3ab254 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Jan 27 14:14:30 2025 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Jan 27 18:32:18 2025 +0100
@@ -121,6 +121,8 @@
   val set_polarity: bool -> Proof.context -> Proof.context
   val set_polarity_generic: bool -> Context.generic -> Context.generic
   val effective_polarity: Proof.context -> bool -> bool
+  val effective_polarity_global: theory -> bool -> bool
+  val effective_polarity_generic: Context.generic -> bool -> bool
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
@@ -787,6 +789,8 @@
 val set_polarity_generic = Config.put_generic polarity;
 
 fun effective_polarity ctxt add = get_polarity ctxt = add;
+fun effective_polarity_global thy add = Config.get_global thy polarity = add;
+val effective_polarity_generic = Context.cases effective_polarity_global effective_polarity;
 
 
 open Lexicon.Syntax;