# HG changeset patch
# User wenzelm
# Date 1703679475 -3600
# Node ID a2d8ecb13d3f37cd05df7d3309719744d833a2e5
# Parent  fe0b52983b7b84d8992accf3207f8b7e92551a64
clarified signature;

diff -r fe0b52983b7b -r a2d8ecb13d3f src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Dec 27 13:02:22 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Wed Dec 27 13:17:55 2023 +0100
@@ -366,7 +366,7 @@
     val (facts', lthy') =
       (facts, lthy) |-> fold_map (fn (a, thms) => fn lthy1 =>
         let
-          val thms1 = name_thms (Local_Theory.bind_name lthy1 (fst a)) thms;
+          val thms1 = name_thms (Local_Theory.full_name_pos lthy1 (fst a)) thms;
           val (thms2, lthy2) =
             (thms1, lthy1) |-> fold_map (fn (args, atts) =>
               fold_map thm_definition args #>> rpair atts);
diff -r fe0b52983b7b -r a2d8ecb13d3f src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Dec 27 13:02:22 2023 +0100
+++ b/src/Pure/Isar/local_theory.ML	Wed Dec 27 13:17:55 2023 +0100
@@ -30,7 +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 full_name_pos: 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
@@ -187,7 +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);
+fun full_name_pos 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 fe0b52983b7b -r a2d8ecb13d3f src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Dec 27 13:02:22 2023 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Dec 27 13:17:55 2023 +0100
@@ -1035,13 +1035,13 @@
 fun update_facts flags (b, SOME ths) ctxt = ctxt |> add_facts flags (b, Lazy.value ths) |> #2
   | update_facts _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b));
 
-fun bind_name ctxt b = (full_name ctxt b, Binding.default_pos_of b);
+fun full_name_pos ctxt b = (full_name ctxt b, Binding.default_pos_of b);
 
 in
 
 fun add_thms_lazy kind (b, ths) ctxt =
   let
-    val name_pos = bind_name ctxt b;
+    val name_pos = full_name_pos ctxt b;
     val ths' =
       Global_Theory.check_thms_lazy ths
       |> Lazy.map_finished
@@ -1051,7 +1051,7 @@
 
 fun note_thms kind ((b, more_atts), facts) ctxt =
   let
-    val name_pos = bind_name ctxt b;
+    val name_pos = full_name_pos ctxt b;
     fun app_fact (thms, atts) =
       fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts)))
         (Global_Theory.name_thms Global_Theory.unofficial1 name_pos thms);
diff -r fe0b52983b7b -r a2d8ecb13d3f src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Wed Dec 27 13:02:22 2023 +0100
+++ b/src/Pure/global_theory.ML	Wed Dec 27 13:17:55 2023 +0100
@@ -257,7 +257,7 @@
 fun add_facts (b, fact) thy =
   let
     val check =
-      Thm_Name.make_list (Sign.bind_name thy b) #> map (fn ((name, pos), thm) =>
+      Thm_Name.make_list (Sign.full_name_pos thy b) #> map (fn ((name, pos), thm) =>
         let
           fun err msg =
             error ("Malformed global fact " ^
@@ -279,7 +279,7 @@
   end;
 
 fun add_thms_lazy kind (b, thms) thy =
-  let val (name, pos) = Sign.bind_name thy b in
+  let val (name, pos) = Sign.full_name_pos thy b in
     if name = "" then register_proofs_lazy (name, pos) thms thy |> #2
     else
       register_proofs_lazy (name, pos)
@@ -299,7 +299,7 @@
 in
 
 fun apply_facts name_flags1 name_flags2 (b, facts) thy =
-  let val (name, pos) = Sign.bind_name thy b in
+  let val (name, pos) = Sign.full_name_pos thy b in
     if name = "" then app_facts facts thy |-> register_proofs (name, pos)
     else
       let
diff -r fe0b52983b7b -r a2d8ecb13d3f src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Dec 27 13:02:22 2023 +0100
+++ b/src/Pure/sign.ML	Wed Dec 27 13:17:55 2023 +0100
@@ -43,7 +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 full_name_pos: 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
@@ -229,7 +229,7 @@
 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);
+fun full_name_pos thy b = (full_name thy b, Binding.default_pos_of b);