# 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 *)