# HG changeset patch
# User wenzelm
# Date 1332185577 -3600
# Node ID f35f654f297d99b24d6db154c6700d5b4396ec4e
# Parent  63e23fc6259bec875a27b895bf7514c5d66bfd04
clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);

diff -r 63e23fc6259b -r f35f654f297d src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Mar 19 19:49:54 2012 +0100
+++ b/src/Pure/General/name_space.ML	Mon Mar 19 20:32:57 2012 +0100
@@ -49,6 +49,7 @@
   val local_naming: naming
   val transform_binding: naming -> binding -> binding
   val full_name: naming -> binding -> string
+  val base_name: binding -> string
   val alias: naming -> binding -> string -> T -> T
   val naming_of: Context.generic -> naming
   val map_naming: (naming -> naming) -> Context.generic -> Context.generic
@@ -314,6 +315,8 @@
 fun full_name naming =
   name_spec naming #> #2 #> map #1 #> Long_Name.implode;
 
+val base_name = full_name default_naming #> Long_Name.base_name;
+
 
 (* accesses *)
 
diff -r 63e23fc6259b -r f35f654f297d src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon Mar 19 19:49:54 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Mon Mar 19 20:32:57 2012 +0100
@@ -178,7 +178,7 @@
     val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
         fold_map Thm.add_axiom_global
           (map (apfst (fn a => Binding.map_name (K a) b))
-            (Global_Theory.name_multi (Variable.check_name b) (map subst props)))
+            (Global_Theory.name_multi (Binding.name_of b) (map subst props)))
         #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
 
     (*facts*)
@@ -328,7 +328,7 @@
   | Element.Obtains obtains =>
       let
         val case_names = obtains |> map_index (fn (i, (b, _)) =>
-          if Binding.is_empty b then string_of_int (i + 1) else Variable.check_name b);
+          if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Element.Constrains
             (vars |> map_filter (fn (x, SOME T) => SOME (Variable.check_name x, T) | _ => NONE)));
diff -r 63e23fc6259b -r f35f654f297d src/Pure/variable.ML
--- a/src/Pure/variable.ML	Mon Mar 19 19:49:54 2012 +0100
+++ b/src/Pure/variable.ML	Mon Mar 19 20:32:57 2012 +0100
@@ -165,8 +165,7 @@
 
 val is_declared = Name.is_declared o names_of;
 
-val check_name =
-  Long_Name.base_name o Name_Space.full_name Name_Space.default_naming o tap Binding.check;
+val check_name = Name_Space.base_name o tap Binding.check;