# HG changeset patch
# User wenzelm
# Date 1237465735 -3600
# Node ID 6b2ba466633625809722c0032f62e325e84c86e6
# Parent  7e839627b9e74e4ae83c2a71220c3e883b30fd45
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);

diff -r 7e839627b9e7 -r 6b2ba4666336 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Mar 19 13:26:19 2009 +0100
+++ b/src/Pure/Isar/class.ML	Thu Mar 19 13:28:55 2009 +0100
@@ -236,7 +236,7 @@
         thy
         |> Sign.declare_const [] ((b, ty0), syn)
         |> snd
-        |> pair ((Binding.name_of b, ty), (c, ty'))
+        |> pair ((Name.of_binding b, ty), (c, ty'))
       end;
   in
     thy
diff -r 7e839627b9e7 -r 6b2ba4666336 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Thu Mar 19 13:26:19 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Thu Mar 19 13:28:55 2009 +0100
@@ -36,7 +36,7 @@
     val prop = prep_prop var_ctxt raw_prop;
     val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
     val _ =
-      (case Option.map Binding.name_of d of
+      (case Option.map Name.of_binding d of
         NONE => ()
       | SOME c' =>
           if c <> c' then
diff -r 7e839627b9e7 -r 6b2ba4666336 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Mar 19 13:26:19 2009 +0100
+++ b/src/Pure/Isar/element.ML	Thu Mar 19 13:28:55 2009 +0100
@@ -96,7 +96,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) =>
-      (Binding.name_of (binding (Binding.name x)), typ T)))
+      (Name.of_binding (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)) =>
diff -r 7e839627b9e7 -r 6b2ba4666336 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Mar 19 13:26:19 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Thu Mar 19 13:28:55 2009 +0100
@@ -125,8 +125,8 @@
 
     val (implicit, expr') = params_expr expr;
 
-    val implicit' = map (#1 #> Binding.name_of) implicit;
-    val fixed' = map (#1 #> Binding.name_of) fixed;
+    val implicit' = map (#1 #> Name.of_binding) implicit;
+    val fixed' = map (#1 #> Name.of_binding) fixed;
     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
     val implicit'' =
       if strict then []
@@ -352,7 +352,7 @@
     fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
       let
         val (parm_names, parm_types) = Locale.params_of thy loc |>
-          map_split (fn (b, SOME T, _) => (Binding.name_of b, T))
+          map_split (fn (b, SOME T, _) => (Name.of_binding b, T))
             (*FIXME return value of Locale.params_of has strange type*)
         val inst' = prep_inst ctxt parm_names inst;
         val parm_types' = map (TypeInfer.paramify_vars o
@@ -386,7 +386,7 @@
       prep_concl raw_concl (insts', elems, ctxt5);
 
     (* Retrieve parameter types *)
-    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.name_of o #1) fixes)
+    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding 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 *)
diff -r 7e839627b9e7 -r 6b2ba4666336 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Mar 19 13:26:19 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Thu Mar 19 13:28:55 2009 +0100
@@ -90,7 +90,7 @@
   let
     val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
     val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
-    val xs = map Binding.name_of bvars;
+    val xs = map Name.of_binding 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 7e839627b9e7 -r 6b2ba4666336 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Mar 19 13:26:19 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Mar 19 13:28:55 2009 +0100
@@ -181,7 +181,7 @@
 fun axioms_of thy = #axioms o the_locale thy;
 
 fun instance_of thy name morph = params_of thy name |>
-  map ((fn (b, T, _) => Free (Binding.name_of b, the T)) #> Morphism.term morph);
+  map ((fn (b, T, _) => Free (Name.of_binding b, the T)) #> Morphism.term morph);
 
 fun specification_of thy = #spec o the_locale thy;
 
diff -r 7e839627b9e7 -r 6b2ba4666336 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Mar 19 13:26:19 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Mar 19 13:28:55 2009 +0100
@@ -119,7 +119,7 @@
     (*obtain vars*)
     val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
     val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
-    val xs = map (Binding.name_of o #1) vars;
+    val xs = map (Name.of_binding o #1) vars;
 
     (*obtain asms*)
     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
@@ -258,7 +258,7 @@
 
 fun inferred_type (binding, _, mx) ctxt =
   let
-    val x = Binding.name_of binding;
+    val x = Name.of_binding binding;
     val (T, ctxt') = ProofContext.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 
diff -r 7e839627b9e7 -r 6b2ba4666336 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 19 13:26:19 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 19 13:28:55 2009 +0100
@@ -1003,7 +1003,7 @@
 fun prep_vars prep_typ internal =
   fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
     let
-      val raw_x = Binding.name_of raw_b;
+      val raw_x = Name.of_binding raw_b;
       val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
       val _ = Syntax.is_identifier (no_skolem internal x) orelse
         error ("Illegal variable name: " ^ quote x);
@@ -1113,7 +1113,7 @@
 fun gen_fixes prep raw_vars ctxt =
   let
     val (vars, _) = prep raw_vars ctxt;
-    val (xs', ctxt') = Variable.add_fixes (map (Binding.name_of o #1) vars) ctxt;
+    val (xs', ctxt') = Variable.add_fixes (map (Name.of_binding o #1) vars) ctxt;
     val ctxt'' =
       ctxt'
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
diff -r 7e839627b9e7 -r 6b2ba4666336 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Mar 19 13:26:19 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Mar 19 13:28:55 2009 +0100
@@ -161,7 +161,7 @@
 fun gen_axioms do_print prep raw_vars raw_specs thy =
   let
     val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy);
-    val xs = map (fn ((b, T), _) => (Binding.name_of b, T)) vars;
+    val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars;
 
     (*consts*)
     val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
@@ -171,7 +171,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))
-            (PureThy.name_multi (Binding.name_of b) (map subst props)))
+            (PureThy.name_multi (Name.of_binding b) (map subst props)))
         #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
 
     (*facts*)
@@ -198,7 +198,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Binding.name_of b;
+            val y = Name.of_binding b;
             val _ = x = y orelse
               error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -234,7 +234,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Binding.name_of b;
+            val y = Name.of_binding b;
             val _ = x = y orelse
               error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -292,10 +292,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 Binding.name_of b);
+          if Binding.is_empty b then string_of_int (i + 1) else Name.of_binding b);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Element.Constrains
-            (vars |> map_filter (fn (x, SOME T) => SOME (Binding.name_of x, T) | _ => NONE)));
+            (vars |> map_filter (fn (x, SOME T) => SOME (Name.of_binding x, T) | _ => NONE)));
 
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
         val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -305,7 +305,7 @@
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let
             val bs = map fst vars;
-            val xs = map Binding.name_of bs;
+            val xs = map Name.of_binding bs;
             val props = map fst asms;
             val (Ts, _) = ctxt'
               |> fold Variable.declare_term props
diff -r 7e839627b9e7 -r 6b2ba4666336 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Mar 19 13:26:19 2009 +0100
+++ b/src/Pure/sign.ML	Thu Mar 19 13:28:55 2009 +0100
@@ -434,7 +434,7 @@
 
 fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
-    val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Binding.name_of a, n, mx)) types) syn;
+    val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
     val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
     val tags = [(Markup.theory_nameN, Context.theory_name thy)];
     val tsig' = fold (Type.add_type naming tags) decls tsig;
@@ -445,7 +445,7 @@
 
 fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
-    val syn' = Syntax.update_consts (map Binding.name_of ns) syn;
+    val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
     val tsig' = fold (Type.add_nonterminal naming []) ns tsig;
   in (naming, syn', tsig', consts) end);
 
@@ -456,7 +456,7 @@
   thy |> map_sign (fn (naming, syn, tsig, consts) =>
     let
       val ctxt = ProofContext.init thy;
-      val syn' = Syntax.update_type_gram [(Binding.name_of a, length vs, mx)] syn;
+      val syn' = Syntax.update_type_gram [(Name.of_binding a, length vs, mx)] syn;
       val b = Binding.map_name (Syntax.type_name mx) a;
       val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
         handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
@@ -504,10 +504,10 @@
     val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
     fun prep (raw_b, raw_T, raw_mx) =
       let
-        val (mx_name, mx) = Syntax.const_mixfix (Binding.name_of raw_b) raw_mx;
+        val (mx_name, mx) = Syntax.const_mixfix (Name.of_binding raw_b) raw_mx;
         val b = Binding.map_name (K mx_name) raw_b;
         val c = full_name thy b;
-        val c_syn = if authentic then Syntax.constN ^ c else Binding.name_of b;
+        val c_syn = if authentic then Syntax.constN ^ c else Name.of_binding b;
         val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
           cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
         val T' = Logic.varifyT T;
@@ -568,7 +568,7 @@
 fun primitive_class (bclass, classes) thy =
   thy |> map_sign (fn (naming, syn, tsig, consts) =>
     let
-      val syn' = Syntax.update_consts [Binding.name_of bclass] syn;
+      val syn' = Syntax.update_consts [Name.of_binding bclass] syn;
       val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
     in (naming, syn', tsig', consts) end)
   |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];