# HG changeset patch
# User haftmann
# Date 1755019004 -7200
# Node ID 157aaea4c42cf46db9caeba6835702646a6c4e2b
# Parent  af4cad931c51ad91ceb85e688ec19263cc6a225c
proper naming for definitions in nested context based upon class target

diff -r af4cad931c51 -r 157aaea4c42c src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
--- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Tue Aug 12 19:16:41 2025 +0200
+++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Tue Aug 12 19:16:44 2025 +0200
@@ -81,8 +81,6 @@
 qualified definition Gcd :: "'a set \<Rightarrow> 'a"
   where [code del]: "Gcd A = Lcm {d. \<forall>a\<in>A. d dvd a}"
 
-end    
-
 lemma semiring_gcd:
   "class.semiring_gcd one zero times gcd lcm
     divide plus minus unit_factor normalize"
@@ -193,7 +191,10 @@
   qed
 qed
 
-interpretation semiring_Gcd one zero times gcd lcm Gcd Lcm
+end
+
+interpretation semiring_Gcd one zero times
+    Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
     divide plus minus unit_factor normalize
   by (fact semiring_Gcd)
 
@@ -269,17 +270,15 @@
 qed
 
 lemma Gcd_eucl_set [code]:
-  "Gcd (set xs) = fold gcd xs 0"
+  "Euclidean_Algorithm.Gcd (set xs) = fold Euclidean_Algorithm.gcd xs 0"
   by (fact Gcd_set_eq_fold)
 
 lemma Lcm_eucl_set [code]:
-  "Lcm (set xs) = fold lcm xs 1"
+  "Euclidean_Algorithm.Lcm (set xs) = fold Euclidean_Algorithm.lcm xs 1"
   by (fact Lcm_set_eq_fold)
  
 end
 
-hide_const (open) gcd lcm Gcd Lcm
-
 lemma prime_elem_int_abs_iff [simp]:
   fixes p :: int
   shows "prime_elem \<bar>p\<bar> \<longleftrightarrow> prime_elem p"
diff -r af4cad931c51 -r 157aaea4c42c src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 12 19:16:41 2025 +0200
+++ b/src/HOL/List.thy	Tue Aug 12 19:16:44 2025 +0200
@@ -8249,8 +8249,6 @@
 
 end
 
-hide_const (open) range \<comment> \<open>TODO: should not be necessary\<close>
-
 instance nat :: discrete_linordered_semidom_with_range
   by standard auto
 
diff -r af4cad931c51 -r 157aaea4c42c src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Aug 12 19:16:41 2025 +0200
+++ b/src/Pure/Isar/class.ML	Tue Aug 12 19:16:44 2025 +0200
@@ -412,12 +412,13 @@
 fun const class ((b, mx), lhs) params lthy =
   let
     val phi = morphism lthy class;
+    val b_canonical = b |> Name_Space.transform_binding (Proof_Context.naming_of lthy);
     val dangling_params = map (Morphism.term phi) (uncurry append (dangling_params_for lthy class params));
   in
     lthy
     |> target_const class phi Syntax.mode_default (b, lhs)
     |> Local_Theory.raw_theory (canonical_const class phi dangling_params
-         ((Morphism.binding phi b, if null dangling_params then mx else NoSyn), Morphism.term phi lhs))
+         ((Morphism.binding phi b_canonical, if null dangling_params then mx else NoSyn), Morphism.term phi lhs))
     |> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other)
          Syntax.mode_default ((b, if null dangling_params then NoSyn else mx), lhs)
     |> synchronize_class_syntax_target class