tuned signature, disentangled dependencies;

--- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Apr 15 15:33:57 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sat Apr 16 12:46:18 2011 +0200
@@ -51,7 +51,7 @@
 
     fun sanity_test NONE _ = true
       | sanity_test (SOME bind) str =
-          if Name.of_binding bind = str then true
+          if Variable.name bind = str then true
           else error_msg bind str
 
     val _ = sanity_test optbind lhs_str

--- a/src/Pure/Isar/class_declaration.ML	Fri Apr 15 15:33:57 2011 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Sat Apr 16 12:46:18 2011 +0200
@@ -255,7 +255,7 @@
         thy
         |> Sign.declare_const ((b, ty0), syn)
         |> snd
-        |> pair ((Name.of_binding b, ty), (c, ty'))
+        |> pair ((Variable.name b, ty), (c, ty'))
       end;
   in
     thy

--- a/src/Pure/Isar/element.ML	Fri Apr 15 15:33:57 2011 +0200
+++ b/src/Pure/Isar/element.ML	Sat Apr 16 12:46:18 2011 +0200
@@ -99,7 +99,7 @@
 fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
   fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
    | Constrains xs => Constrains (xs |> map (fn (x, T) =>
-      (Name.of_binding (binding (Binding.name x)), typ T)))
+      (Variable.name (binding (Binding.name x)), typ T)))
    | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
       ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
    | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
@@ -526,7 +526,7 @@
 
 fun activate raw_elem ctxt =
   let val elem = raw_elem |> map_ctxt
-   {binding = tap Name.of_binding,
+   {binding = tap Variable.name,
     typ = I,
     term = I,
     pattern = I,

--- a/src/Pure/Isar/expression.ML	Fri Apr 15 15:33:57 2011 +0200
+++ b/src/Pure/Isar/expression.ML	Sat Apr 16 12:46:18 2011 +0200
@@ -128,7 +128,7 @@
     val (implicit, expr') = params_expr expr;
 
     val implicit' = map #1 implicit;
-    val fixed' = map (#1 #> Name.of_binding) fixed;
+    val fixed' = map (Variable.name o #1) fixed;
     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
     val implicit'' =
       if strict then []
@@ -395,7 +395,7 @@
     val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
 
     (* Retrieve parameter types *)
-    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding o #1) fixes)
+    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.name o #1) fixes)
       | _ => fn ps => ps) (Fixes fors :: elems') [];
     val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6;
     val parms = xs ~~ Ts;  (* params from expression and elements *)

--- a/src/Pure/Isar/local_defs.ML	Fri Apr 15 15:33:57 2011 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sat Apr 16 12:46:18 2011 +0200
@@ -92,7 +92,7 @@
   let
     val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
     val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
-    val xs = map Name.of_binding bvars;
+    val xs = map Variable.name bvars;
     val names = map2 Thm.def_binding_optional bvars bfacts;
     val eqs = mk_def ctxt (xs ~~ rhss);
     val lhss = map (fst o Logic.dest_equals) eqs;

--- a/src/Pure/Isar/obtain.ML	Fri Apr 15 15:33:57 2011 +0200
+++ b/src/Pure/Isar/obtain.ML	Sat Apr 16 12:46:18 2011 +0200
@@ -119,7 +119,7 @@
     (*obtain vars*)
     val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
     val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
-    val xs = map (Name.of_binding o #1) vars;
+    val xs = map (Variable.name o #1) vars;
 
     (*obtain asms*)
     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
@@ -257,7 +257,7 @@
 
 fun inferred_type (binding, _, mx) ctxt =
   let
-    val x = Name.of_binding binding;
+    val x = Variable.name binding;
     val (T, ctxt') = ProofContext.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 

--- a/src/Pure/Isar/proof_context.ML	Fri Apr 15 15:33:57 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 16 12:46:18 2011 +0200
@@ -923,7 +923,7 @@
 fun prep_vars prep_typ internal =
   fold_map (fn (b, raw_T, mx) => fn ctxt =>
     let
-      val x = Name.of_binding b;
+      val x = Variable.name b;
       val _ = Lexicon.is_identifier (no_skolem internal x) orelse
         error ("Illegal variable name: " ^ quote (Binding.str_of b));
 
@@ -1023,7 +1023,7 @@
 fun add_fixes raw_vars ctxt =
   let
     val (vars, _) = cert_vars raw_vars ctxt;
-    val (xs', ctxt') = Variable.add_fixes (map (Name.of_binding o #1) vars) ctxt;
+    val (xs', ctxt') = Variable.add_fixes (map (Variable.name o #1) vars) ctxt;
     val ctxt'' =
       ctxt'
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)

--- a/src/Pure/Isar/specification.ML	Fri Apr 15 15:33:57 2011 +0200
+++ b/src/Pure/Isar/specification.ML	Sat Apr 16 12:46:18 2011 +0200
@@ -172,7 +172,7 @@
 fun gen_axioms do_print prep raw_vars raw_specs thy =
   let
     val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init_global thy);
-    val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars;
+    val xs = map (fn ((b, T), _) => (Variable.name b, T)) vars;
 
     (*consts*)
     val (consts, consts_thy) = thy |> fold_map Theory.specify_const vars;
@@ -182,7 +182,7 @@
     val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
         fold_map Thm.add_axiom
           (map (apfst (fn a => Binding.map_name (K a) b))
-            (Global_Theory.name_multi (Name.of_binding b) (map subst props)))
+            (Global_Theory.name_multi (Variable.name b) (map subst props)))
         #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
 
     (*facts*)
@@ -214,7 +214,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Name.of_binding b;
+            val y = Variable.name b;
             val _ = x = y orelse
               error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -253,7 +253,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Name.of_binding b;
+            val y = Variable.name b;
             val _ = x = y orelse
               error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -323,10 +323,10 @@
   | 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 Name.of_binding b);
+          if Binding.is_empty b then string_of_int (i + 1) else Variable.name b);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Element.Constrains
-            (vars |> map_filter (fn (x, SOME T) => SOME (Name.of_binding x, T) | _ => NONE)));
+            (vars |> map_filter (fn (x, SOME T) => SOME (Variable.name x, T) | _ => NONE)));
 
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
         val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -336,7 +336,7 @@
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let
             val bs = map fst vars;
-            val xs = map Name.of_binding bs;
+            val xs = map Variable.name bs;
             val props = map fst asms;
             val (Ts, _) = ctxt'
               |> fold Variable.declare_term props

--- a/src/Pure/ROOT.ML	Fri Apr 15 15:33:57 2011 +0200
+++ b/src/Pure/ROOT.ML	Sat Apr 16 12:46:18 2011 +0200
@@ -46,7 +46,6 @@
 use "General/linear_set.ML";
 use "General/long_name.ML";
 use "General/binding.ML";
-use "General/name_space.ML";
 use "General/path.ML";
 use "General/url.ML";
 use "General/buffer.ML";
@@ -111,6 +110,7 @@
 use "context.ML";
 use "config.ML";
 use "context_position.ML";
+use "General/name_space.ML";
 use "sorts.ML";
 use "type.ML";
 use "logic.ML";

--- a/src/Pure/name.ML	Fri Apr 15 15:33:57 2011 +0200
+++ b/src/Pure/name.ML	Sat Apr 16 12:46:18 2011 +0200
@@ -8,7 +8,6 @@
 sig
   val uu: string
   val aT: string
-  val of_binding: binding -> string
   val bound: int -> string
   val is_bound: string -> bool
   val internal: string -> string
@@ -43,11 +42,6 @@
 
 (** special variable names **)
 
-(* checked binding *)
-
-val of_binding = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
-
-
 (* encoded bounds *)
 
 (*names for numbered variables --

--- a/src/Pure/variable.ML	Fri Apr 15 15:33:57 2011 +0200
+++ b/src/Pure/variable.ML	Sat Apr 16 12:46:18 2011 +0200
@@ -19,6 +19,7 @@
   val is_fixed: Proof.context -> string -> bool
   val newly_fixed: Proof.context -> Proof.context -> string -> bool
   val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
+  val name: binding -> string
   val default_type: Proof.context -> string -> typ option
   val def_type: Proof.context -> bool -> indexname -> typ option
   val def_sort: Proof.context -> indexname -> sort option
@@ -155,6 +156,9 @@
 fun add_fixed ctxt = Term.fold_aterms
   (fn Free (x, T) => if is_fixed ctxt x then insert (op =) (x, T) else I | _ => I);
 
+(*checked name binding*)
+val name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
+
 
 
 (** declarations **)