using name bindings

--- a/src/Pure/Isar/class.ML	Thu Nov 20 14:51:40 2008 +0100
+++ b/src/Pure/Isar/class.ML	Thu Nov 20 14:55:25 2008 +0100
@@ -513,7 +513,7 @@
     val ty' = Term.fastype_of rhs';
   in
     thy'
-    |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs'') |> snd
+    |> Sign.add_abbrev (#1 prmode) pos (Name.binding c, map_types Type.strip_sorts rhs'') |> snd
     |> Sign.add_const_constraint (c', SOME ty')
     |> Sign.notation true prmode [(Const (c', ty'), mx)]
     |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))

--- a/src/Pure/Isar/proof_context.ML	Thu Nov 20 14:51:40 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Nov 20 14:55:25 2008 +0100
@@ -26,6 +26,7 @@
   val name_decl: (string * 'a -> Proof.context -> 'b * Proof.context)
     -> Name.binding * 'a -> Proof.context -> (string * 'b) * Proof.context
   val full_name: Proof.context -> bstring -> string
+  val full_binding: Proof.context -> Name.binding -> string
   val consts_of: Proof.context -> Consts.T
   val const_syntax_name: Proof.context -> string -> string
   val the_const_constraint: Proof.context -> string -> typ
@@ -136,7 +137,7 @@
     Context.generic -> Context.generic
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   val add_abbrev: string -> Properties.T ->
-    bstring * term -> Proof.context -> (term * term) * Proof.context
+    Name.binding * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
   val verbose: bool ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
@@ -248,19 +249,20 @@
 
 val naming_of = #naming o rep_context;
 
-fun name_decl decl (binding, x) ctxt =
+fun name_decl decl (b, x) ctxt =
   let
     val naming = naming_of ctxt;
-    val (naming', name) = Name.namify naming binding;
+    val (naming', name) = Name.namify naming b;
   in
     ctxt
     |> map_naming (K naming')
-    |> decl (Name.name_of binding, x)
+    |> decl (Name.name_of b, x)
     |>> pair name
     ||> map_naming (K naming)
   end;
 
 val full_name = NameSpace.full o naming_of;
+val full_binding = NameSpace.full_binding o naming_of;
 
 val syntax_of = #syntax o rep_context;
 val syn_of = LocalSyntax.syn_of o syntax_of;
@@ -977,15 +979,14 @@
 
 local
 
-fun update_thms _ (bname, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt bname))
-  | update_thms do_props (bname, SOME ths) ctxt = ctxt |> map_facts
-      (Facts.add_local do_props (naming_of ctxt) (full_name ctxt bname, ths));
+fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_binding ctxt b))
+  | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
+      (Facts.add_local do_props (naming_of ctxt) (full_binding ctxt b, ths));
 
-fun gen_note_thmss get k = fold_map (fn ((binding, more_attrs), raw_facts) => fn ctxt =>
+fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
   let
-    val bname = Name.name_of binding;
-    val pos = Name.pos_of binding;
-    val name = full_name ctxt bname;
+    val pos = Name.pos_of b;
+    val name = full_binding ctxt b;
     val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
 
     val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
@@ -994,7 +995,7 @@
     val (res, ctxt') = fold_map app facts ctxt;
     val thms = PureThy.name_thms false false pos name (flat res);
     val Mode {stmt, ...} = get_mode ctxt;
-  in ((name, thms), ctxt' |> update_thms stmt (bname, SOME thms)) end);
+  in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
 
 in
 
@@ -1004,7 +1005,7 @@
 fun put_thms do_props thms ctxt = ctxt
   |> map_naming (K local_naming)
   |> ContextPosition.set_visible false
-  |> update_thms do_props thms
+  |> update_thms do_props (apfst Name.binding thms)
   |> ContextPosition.restore_visible ctxt
   |> restore_naming ctxt;
 
@@ -1023,9 +1024,9 @@
 local
 
 fun prep_vars prep_typ internal =
-  fold_map (fn (raw_binding, raw_T, raw_mx) => fn ctxt =>
+  fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
     let
-      val raw_x = Name.name_of raw_binding;
+      val raw_x = Name.name_of 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);
@@ -1034,7 +1035,7 @@
         if internal then T
         else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
       val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
-      val var = (Name.map_name (K x) raw_binding, opt_T, mx);
+      val var = (Name.map_name (K x) raw_b, opt_T, mx);
     in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end);
 
 in
@@ -1105,13 +1106,13 @@
       in cert_term ctxt (Const (c, T)); T end;
   in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end;
 
-fun add_abbrev mode tags (c, raw_t) ctxt =
+fun add_abbrev mode tags (b, raw_t) ctxt =
   let
     val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
-      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
+      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b));
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val ((lhs, rhs), consts') = consts_of ctxt
-      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (c, t);
+      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);
   in
     ctxt
     |> (map_consts o apfst) (K consts')
@@ -1140,8 +1141,8 @@
       ctxt'
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
       |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
-    val _ = (vars ~~ xs') |> List.app (fn ((binding, _, _), x') =>
-      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of binding));
+    val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
+      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of b));
   in (xs', ctxt'') end;
 
 in

--- a/src/Pure/Isar/theory_target.ML	Thu Nov 20 14:51:40 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Nov 20 14:55:25 2008 +0100
@@ -1,5 +1,6 @@
 (*  Title:      Pure/Isar/theory_target.ML
     ID:         $Id$
+    ID:         $Id$
     Author:     Makarius
 
 Common theory/locale/class/instantiation/overloading targets.
@@ -192,18 +193,18 @@
   else if not is_class then (NoSyn, mx, NoSyn)
   else (mx, NoSyn, NoSyn);
 
-fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi =
+fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((b, mx), rhs) phi =
   let
-    val c' = Morphism.name phi c;
+    val b' = Morphism.name phi b;
     val rhs' = Morphism.term phi rhs;
-    val name' = Name.name_with_prefix c';
-    val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
-    val arg = (name', Term.close_schematic_term rhs');
+    val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
+    val arg = (b', Term.close_schematic_term rhs');
     val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
-    val class_global = Name.name_of c = Name.name_of c'
-      andalso not (null (Name.prefix_of c'))
-      andalso (fst o snd o split_last) (Name.prefix_of c') = Class.class_prefix target;
+    val (prefix', _) = Name.dest_binding b';
+    val class_global = Name.name_of b = Name.name_of b'
+      andalso not (null prefix')
+      andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
@@ -267,7 +268,7 @@
   in
     lthy |>
      (if is_locale then
-        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (c, global_rhs))
+        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (b, global_rhs))
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
             term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
@@ -275,9 +276,9 @@
           end)
       else
         LocalTheory.theory
-          (Sign.add_abbrev (#1 prmode) tags (c, global_rhs) #-> (fn (lhs, _) =>
+          (Sign.add_abbrev (#1 prmode) tags (b, global_rhs) #-> (fn (lhs, _) =>
            Sign.notation true prmode [(lhs, mx3)])))
-    |> ProofContext.add_abbrev PrintMode.internal tags (c, t) |> snd
+    |> ProofContext.add_abbrev PrintMode.internal tags (b, t) |> snd
     |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
   end;
 

--- a/src/Pure/consts.ML	Thu Nov 20 14:51:40 2008 +0100
+++ b/src/Pure/consts.ML	Thu Nov 20 14:55:25 2008 +0100
@@ -30,10 +30,10 @@
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: bool -> NameSpace.naming -> Properties.T -> (bstring * typ) -> T -> T
+  val declare: bool -> NameSpace.naming -> Properties.T -> (Name.binding * typ) -> T -> T
   val constrain: string * typ option -> T -> T
   val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
-    bstring * term -> T -> (term * term) * T
+    Name.binding * term -> T -> (term * term) * T
   val revert_abbrev: string -> string -> T -> T
   val hide: bool -> string -> T -> T
   val empty: T
@@ -211,7 +211,7 @@
 fun err_dup_const c =
   error ("Duplicate declaration of constant " ^ quote c);
 
-fun extend_decls naming decl tab = NameSpace.extend_table naming [decl] tab
+fun extend_decls naming decl tab = NameSpace.table_declare naming decl tab
   handle Symtab.DUP c => err_dup_const c;
 
 
@@ -223,11 +223,11 @@
 
 (* declarations *)
 
-fun declare authentic naming tags (c, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
+fun declare authentic naming tags (b, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
   let
     val tags' = tags |> Position.default_properties (Position.thread_data ());
     val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
-    val decls' = decls |> extend_decls naming (c, ((decl, NONE), serial ()));
+    val (_, decls') = decls |> extend_decls naming (b, ((decl, NONE), serial ()));
   in (decls', constraints, rev_abbrevs) end);
 
 
@@ -262,7 +262,7 @@
 
 in
 
-fun abbreviate pp tsig naming mode tags (c, raw_rhs) consts =
+fun abbreviate pp tsig naming mode tags (b, raw_rhs) consts =
   let
     val cert_term = certify pp tsig false consts;
     val expand_term = certify pp tsig true consts;
@@ -273,7 +273,7 @@
       |> cert_term;
     val normal_rhs = expand_term rhs;
     val T = Term.fastype_of rhs;
-    val lhs = Const (NameSpace.full naming c, T);
+    val lhs = Const (NameSpace.full_binding naming b, T);
 
     fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
       Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));
@@ -285,8 +285,8 @@
         val tags' = tags |> Position.default_properties (Position.thread_data ());
         val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
-        val decls' = decls
-          |> extend_decls naming (c, ((decl, SOME abbr), serial ()));
+        val (_, decls') = decls
+          |> extend_decls naming (b, ((decl, SOME abbr), serial ()));
         val rev_abbrevs' = rev_abbrevs
           |> fold (curry Symtab.cons_list mode) (rev_abbrev lhs rhs);
       in (decls', constraints, rev_abbrevs') end)

--- a/src/Pure/pure_thy.ML	Thu Nov 20 14:51:40 2008 +0100
+++ b/src/Pure/pure_thy.ML	Thu Nov 20 14:55:25 2008 +0100
@@ -143,35 +143,36 @@
 fun enter_proofs (thy, thms) =
   (FactsData.map (apsnd (fold (cons o lazy_proof) thms)) thy, thms);
 
-fun enter_thms _ _ app_att ("", thms) thy = swap (enter_proofs (app_att (thy, thms)))
-  | enter_thms pre_name post_name app_att (bname, thms) thy =
-      let
-        val naming = Sign.naming_of thy;
-        val name = NameSpace.full naming bname;
-        val (thy', thms') =
-          enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
-        val thms'' = map (Thm.transfer thy') thms';
-        val thy'' = thy' |> FactsData.map (apfst (Facts.add_global naming (name, thms'')));
-      in (thms'', thy'') end;
+fun enter_thms pre_name post_name app_att (b, thms) thy =
+  if Name.is_nothing b
+  then swap (enter_proofs (app_att (thy, thms)))
+  else let
+    val naming = Sign.naming_of thy;
+    val name = NameSpace.full_binding naming b;
+    val (thy', thms') =
+      enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
+    val thms'' = map (Thm.transfer thy') thms';
+    val thy'' = thy' |> FactsData.map (apfst (Facts.add_global naming (name, thms'')));
+  in (thms'', thy'') end;
 
 
 (* store_thm(s) *)
 
-val store_thms =
-  enter_thms (name_thms true true Position.none) (name_thms false true Position.none) I;
+fun store_thms (bname, thms) = enter_thms (name_thms true true Position.none)
+  (name_thms false true Position.none) I (Name.binding bname, thms);
 
-fun store_thm (name, th) = store_thms (name, [th]) #>> the_single;
+fun store_thm (bname, th) = store_thms (bname, [th]) #>> the_single;
 
-fun store_thm_open (name, th) =
+fun store_thm_open (bname, th) =
   enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I
-    (name, [th]) #>> the_single;
+    (Name.binding bname, [th]) #>> the_single;
 
 
 (* add_thms(s) *)
 
 fun add_thms_atts pre_name ((bname, thms), atts) =
   enter_thms pre_name (name_thms false true Position.none)
-    (foldl_map (Thm.theory_attributes atts)) (bname, thms);
+    (foldl_map (Thm.theory_attributes atts)) (Name.binding bname, thms);
 
 fun gen_add_thmss pre_name =
   fold_map (add_thms_atts pre_name);
@@ -195,17 +196,16 @@
 
 local
 
-fun gen_note_thmss tag = fold_map (fn ((binding, more_atts), ths_atts) => fn thy =>
+fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
   let
-    val bname = Name.name_of binding;
-    val pos = Name.pos_of binding;
-    val name = Sign.full_name thy bname;
+    val pos = Name.pos_of b;
+    val name = Sign.full_binding thy b;
     val _ = Position.report (Markup.fact_decl name) pos;
 
     fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
     val (thms, thy') = thy |> enter_thms
       (name_thmss true pos) (name_thms false true pos) (apsnd flat o foldl_map app)
-      (bname, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts);
+      (b, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts);
   in ((name, thms), thy') end);
 
 in

--- a/src/Pure/sign.ML	Thu Nov 20 14:51:40 2008 +0100
+++ b/src/Pure/sign.ML	Thu Nov 20 14:55:25 2008 +0100
@@ -18,6 +18,7 @@
   val name_decl: (string * 'a -> theory -> 'b * theory)
     -> Name.binding * 'a -> theory -> (string * 'b) * theory
   val full_name: theory -> bstring -> string
+  val full_binding: theory -> Name.binding -> string
   val full_name_path: theory -> string -> bstring -> string
   val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
   val syn_of: theory -> Syntax.syntax
@@ -93,10 +94,10 @@
   val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
   val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
+  val declare_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
   val add_consts: (bstring * string * mixfix) list -> theory -> theory
   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
-  val declare_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
-  val add_abbrev: string -> Properties.T -> bstring * term -> theory -> (term * term) * theory
+  val add_abbrev: string -> Properties.T -> Name.binding * term -> theory -> (term * term) * theory
   val revert_abbrev: string -> string -> theory -> theory
   val add_const_constraint: string * typ option -> theory -> theory
   val primitive_class: string * class list -> theory -> theory
@@ -190,20 +191,21 @@
 val naming_of = #naming o rep_sg;
 val base_name = NameSpace.base;
 
-fun name_decl decl (binding, x) thy =
+fun name_decl decl (b, x) thy =
   let
     val naming = naming_of thy;
-    val (naming', name) = Name.namify naming binding;
+    val (naming', name) = Name.namify naming b;
   in
     thy
     |> map_naming (K naming')
-    |> decl (Name.name_of binding, x)
+    |> decl (Name.name_of b, x)
     |>> pair name
     ||> map_naming (K naming)
   end;
 
 val namify = Name.namify o naming_of;
 val full_name = NameSpace.full o naming_of;
+val full_binding = NameSpace.full_binding o naming_of;
 fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));
 val declare_name = NameSpace.declare o naming_of;
 
@@ -520,15 +522,16 @@
   let
     val ctxt = ProofContext.init thy;
     val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
-    fun prep (raw_c, raw_T, raw_mx) =
+    fun prep (raw_b, raw_T, raw_mx) =
       let
-        val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
-        val full_c = full_name thy c;
-        val c' = if authentic then Syntax.constN ^ full_c else c;
+        val (mx_name, mx) = Syntax.const_mixfix (Name.name_of raw_b) raw_mx;
+        val b = Name.map_name (K mx_name) raw_b;
+        val c = full_binding thy b;
+        val c_syn = if authentic then Syntax.constN ^ c else Name.name_of b;
         val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
-          cat_error msg ("in declaration of constant " ^ quote c);
+          cat_error msg ("in declaration of constant " ^ quote (Name.display b));
         val T' = Logic.varifyT T;
-      in ((c, T'), (c', T', mx), Const (full_c, T)) end;
+      in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
     val args = map prep raw_args;
     val tags' = tags |> Properties.put (Markup.theory_nameN, Context.theory_name thy);
   in
@@ -538,18 +541,19 @@
     |> pair (map #3 args)
   end;
 
+fun bindify (name, T, mx) = (Name.binding name, T, mx);
+
 in
 
-val add_consts = snd oo gen_add_consts Syntax.parse_typ false [];
-val add_consts_i = snd oo gen_add_consts (K I) false [];
+fun add_consts args = snd o gen_add_consts Syntax.parse_typ false [] (map bindify args);
+fun add_consts_i args = snd o gen_add_consts (K I) false [] (map bindify args);
 
 fun declare_const tags ((b, T), mx) thy =
   let
-    val c = Name.name_of b;
     val pos = Name.pos_of b;
     val tags' = Position.default_properties pos tags;
-    val ([const as Const (full_c, _)], thy') = gen_add_consts (K I) true tags' [(c, T, mx)] thy;
-    val _ = Position.report (Markup.const_decl full_c) pos;
+    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy;
+    val _ = Position.report (Markup.const_decl c) pos;
   in (const, thy') end;
 
 end;
@@ -557,14 +561,14 @@
 
 (* abbreviations *)
 
-fun add_abbrev mode tags (c, raw_t) thy =
+fun add_abbrev mode tags (b, raw_t) thy =
   let
     val pp = Syntax.pp_global thy;
     val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
-      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
+      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b));
     val (res, consts') = consts_of thy
-      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (c, t);
+      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
   in (res, thy |> map_consts (K consts')) end;
 
 fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);