# HG changeset patch
# User wenzelm
# Date 1303930720 -7200
# Node ID eef1a23c9077efcc9cda06003e4f5e6fc66d02f3
# Parent  01430341fc799ae9afea7857b24af122b971d666
tuned signature -- eliminated odd comment;

diff -r 01430341fc79 -r eef1a23c9077 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Wed Apr 27 20:37:56 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Wed Apr 27 20:58:40 2011 +0200
@@ -51,7 +51,7 @@
 
     fun sanity_test NONE _ = true
       | sanity_test (SOME bind) str =
-          if Variable.name bind = str then true
+          if Variable.check_name bind = str then true
           else error_msg bind str
 
     val _ = sanity_test optbind lhs_str
diff -r 01430341fc79 -r eef1a23c9077 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Wed Apr 27 20:58:40 2011 +0200
@@ -254,7 +254,7 @@
         thy
         |> Sign.declare_const_global ((b, ty0), syn)
         |> snd
-        |> pair ((Variable.name b, ty), (c, ty'))
+        |> pair ((Variable.check_name b, ty), (c, ty'))
       end;
   in
     thy
diff -r 01430341fc79 -r eef1a23c9077 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/element.ML	Wed Apr 27 20:58:40 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) =>
-      (Variable.name (binding (Binding.name x)), typ T)))
+      (Variable.check_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 Variable.name,
+   {binding = tap Variable.check_name,
     typ = I,
     term = I,
     pattern = I,
diff -r 01430341fc79 -r eef1a23c9077 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Apr 27 20:58:40 2011 +0200
@@ -128,7 +128,7 @@
     val (implicit, expr') = params_expr expr;
 
     val implicit' = map #1 implicit;
-    val fixed' = map (Variable.name o #1) fixed;
+    val fixed' = map (Variable.check_name o #1) fixed;
     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
     val implicit'' =
       if strict then []
@@ -393,7 +393,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 (Variable.name o #1) fixes)
+    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.check_name o #1) fixes)
       | _ => fn ps => ps) (Fixes fors :: elems') [];
     val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
     val parms = xs ~~ Ts;  (* params from expression and elements *)
diff -r 01430341fc79 -r eef1a23c9077 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Apr 27 20:58:40 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 Variable.name bvars;
+    val xs = map Variable.check_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;
diff -r 01430341fc79 -r eef1a23c9077 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Apr 27 20:58:40 2011 +0200
@@ -119,7 +119,7 @@
     (*obtain vars*)
     val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
     val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
-    val xs = map (Variable.name o #1) vars;
+    val xs = map (Variable.check_name o #1) vars;
 
     (*obtain asms*)
     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
@@ -255,7 +255,7 @@
 
 fun inferred_type (binding, _, mx) ctxt =
   let
-    val x = Variable.name binding;
+    val x = Variable.check_name binding;
     val (T, ctxt') = Proof_Context.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 
diff -r 01430341fc79 -r eef1a23c9077 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 27 20:58:40 2011 +0200
@@ -928,7 +928,7 @@
 fun prep_vars prep_typ internal =
   fold_map (fn (b, raw_T, mx) => fn ctxt =>
     let
-      val x = Variable.name b;
+      val x = Variable.check_name b;
       val _ = Lexicon.is_identifier (no_skolem internal x) orelse
         error ("Illegal variable name: " ^ Binding.print b);
 
diff -r 01430341fc79 -r eef1a23c9077 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Apr 27 20:58:40 2011 +0200
@@ -169,7 +169,7 @@
 fun gen_axioms do_print prep raw_vars raw_specs thy =
   let
     val ((vars, specs), _) = prep raw_vars raw_specs (Proof_Context.init_global thy);
-    val xs = map (fn ((b, T), _) => (Variable.name b, T)) vars;
+    val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) vars;
 
     (*consts*)
     val (consts, consts_thy) = thy |> fold_map Theory.specify_const vars;
@@ -179,7 +179,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.name b) (map subst props)))
+            (Global_Theory.name_multi (Variable.check_name b) (map subst props)))
         #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
 
     (*facts*)
@@ -211,7 +211,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Variable.name b;
+            val y = Variable.check_name b;
             val _ = x = y orelse
               error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -250,7 +250,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Variable.name b;
+            val y = Variable.check_name b;
             val _ = x = y orelse
               error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -320,10 +320,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 Variable.name b);
+          if Binding.is_empty b then string_of_int (i + 1) else Variable.check_name b);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Element.Constrains
-            (vars |> map_filter (fn (x, SOME T) => SOME (Variable.name x, T) | _ => NONE)));
+            (vars |> map_filter (fn (x, SOME T) => SOME (Variable.check_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;
@@ -333,7 +333,7 @@
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let
             val bs = map fst vars;
-            val xs = map Variable.name bs;
+            val xs = map Variable.check_name bs;
             val props = map fst asms;
             val (Ts, _) = ctxt'
               |> fold Variable.declare_term props
diff -r 01430341fc79 -r eef1a23c9077 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/variable.ML	Wed Apr 27 20:58:40 2011 +0200
@@ -15,7 +15,7 @@
   val sorts_of: Proof.context -> sort list
   val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table
   val is_declared: Proof.context -> string -> bool
-  val name: binding -> string
+  val check_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
@@ -164,8 +164,7 @@
 
 val is_declared = Name.is_declared o names_of;
 
-(*checked name binding*)
-val name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
+val check_name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
 
 
 
@@ -362,7 +361,7 @@
         [] => ()
       | dups => err_dups dups);
 
-    val xs = map name bs;
+    val xs = map check_name bs;
     val names = names_of ctxt;
     val (xs', names') =
       if is_body ctxt then Name.variants xs names |>> map Name.skolem