# HG changeset patch
# User wenzelm
# Date 1726505979 -7200
# Node ID c012dfcab50f1993096307ec3886d9c95cacf714
# Parent  5d562dd387aea03c00a4ff2797da5c05a2cd26dc
clarified name space: no theory qualifier here --- treat like global datatype constructors;

diff -r 5d562dd387ae -r c012dfcab50f src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Mon Sep 16 15:49:36 2024 +0200
+++ b/src/Pure/Thy/term_style.ML	Mon Sep 16 18:59:39 2024 +0200
@@ -25,7 +25,8 @@
 val get_data = Data.get o Proof_Context.theory_of;
 
 fun setup binding style thy =
-  Data.map (#2 o Name_Space.define (Context.Theory thy) true (binding, style)) thy;
+  let val context = Name_Space.map_naming (K Name_Space.global_naming) (Context.Theory thy)
+  in Data.map (#2 o Name_Space.define context true (binding, style)) thy end;
 
 
 (* style parsing *)