# HG changeset patch
# User wenzelm
# Date 1703415119 -3600
# Node ID 75701d767ed9b63a0f76b274489d4114be1b14a2
# Parent  704aea7f5203043e1c4d0a629cf41506bc371725
clarified modules;

diff -r 704aea7f5203 -r 75701d767ed9 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Dec 24 11:46:20 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sun Dec 24 11:51:59 2023 +0100
@@ -349,9 +349,6 @@
 
   in (result'', result) end;
 
-fun bind_name lthy b =
-  (Local_Theory.full_name lthy b, Binding.default_pos_of b);
-
 fun map_facts f = (map o apsnd o map o apfst o map) f;
 
 in
@@ -360,7 +357,7 @@
   let
     val facts' = facts |> map (fn (a, thms) =>
       let
-        val name_pos = bind_name lthy (fst a);
+        val name_pos = Local_Theory.bind_name lthy (fst a);
         val thms' = Global_Theory.burrow_fact (Global_Theory.name_multi name_pos) thms;
       in (a, (map o apfst o map) (import_export_proof lthy) thms') end);
     val local_facts = map_facts #1 facts';
diff -r 704aea7f5203 -r 75701d767ed9 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun Dec 24 11:46:20 2023 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sun Dec 24 11:51:59 2023 +0100
@@ -30,6 +30,7 @@
     local_theory -> local_theory
   val restore_background_naming: local_theory -> local_theory -> local_theory
   val full_name: local_theory -> binding -> string
+  val bind_name: local_theory -> binding -> string * Position.T
   val new_group: local_theory -> local_theory
   val reset_group: local_theory -> local_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
@@ -186,6 +187,7 @@
 val restore_background_naming = map_background_naming o K o background_naming_of;
 
 val full_name = Name_Space.full_name o background_naming_of;
+fun bind_name lthy b = (full_name lthy b, Binding.default_pos_of b);
 
 val new_group = map_background_naming Name_Space.new_group;
 val reset_group = map_background_naming Name_Space.reset_group;
diff -r 704aea7f5203 -r 75701d767ed9 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sun Dec 24 11:46:20 2023 +0100
+++ b/src/Pure/global_theory.ML	Sun Dec 24 11:51:59 2023 +0100
@@ -267,11 +267,9 @@
 
 (* store theorems and proofs *)
 
-fun bind_name thy b = (Sign.full_name thy b, Binding.default_pos_of b);
-
 fun add_facts (b, fact) thy =
   let
-    val (full_name, pos) = bind_name thy b;
+    val (full_name, pos) = Sign.bind_name thy b;
     fun check fact =
       fact |> map_index (fn (i, thm) =>
         let
@@ -297,7 +295,7 @@
   end;
 
 fun add_thms_lazy kind (b, thms) thy =
-  let val (name, pos) = bind_name thy b in
+  let val (name, pos) = Sign.bind_name thy b in
     if name = "" then register_proofs_lazy (name, pos) thms thy |> #2
     else
       register_proofs_lazy (name, pos)
@@ -317,11 +315,11 @@
 in
 
 fun apply_facts name_flags1 name_flags2 (b, facts) thy =
-  let val (name, pos) = bind_name thy b in
+  let val (name, pos) = Sign.bind_name thy b in
     if name = "" then app_facts facts thy |-> register_proofs (name, pos)
     else
       let
-        val name_pos = bind_name thy b;
+        val name_pos = Sign.bind_name thy b;
         val (thms', thy') = thy
           |> app_facts (map (apfst (name_thms name_flags1 name_pos)) facts)
           |>> name_thms name_flags2 name_pos |-> register_proofs (name, pos);
diff -r 704aea7f5203 -r 75701d767ed9 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Dec 24 11:46:20 2023 +0100
+++ b/src/Pure/sign.ML	Sun Dec 24 11:51:59 2023 +0100
@@ -43,6 +43,7 @@
   val full_name_path: theory -> string -> binding -> string
   val full_bname: theory -> bstring -> string
   val full_bname_path: theory -> string -> bstring -> string
+  val bind_name: theory -> binding -> string * Position.T
   val const_monomorphic: theory -> string -> bool
   val const_typargs: theory -> string * typ -> typ list
   val const_instance: theory -> string * typ list -> typ
@@ -228,6 +229,8 @@
 fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
 fun full_bname_path thy path = full_name_path thy path o Binding.name;
 
+fun bind_name thy b = (full_name thy b, Binding.default_pos_of b);
+
 
 
 (** name spaces **)