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

     2.1 --- a/src/Pure/Isar/proof_context.ML	Thu Nov 20 14:51:40 2008 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Nov 20 14:55:25 2008 +0100
     2.3 @@ -26,6 +26,7 @@
     2.4    val name_decl: (string * 'a -> Proof.context -> 'b * Proof.context)
     2.5      -> Name.binding * 'a -> Proof.context -> (string * 'b) * Proof.context
     2.6    val full_name: Proof.context -> bstring -> string
     2.7 +  val full_binding: Proof.context -> Name.binding -> string
     2.8    val consts_of: Proof.context -> Consts.T
     2.9    val const_syntax_name: Proof.context -> string -> string
    2.10    val the_const_constraint: Proof.context -> string -> typ
    2.11 @@ -136,7 +137,7 @@
    2.12      Context.generic -> Context.generic
    2.13    val add_const_constraint: string * typ option -> Proof.context -> Proof.context
    2.14    val add_abbrev: string -> Properties.T ->
    2.15 -    bstring * term -> Proof.context -> (term * term) * Proof.context
    2.16 +    Name.binding * term -> Proof.context -> (term * term) * Proof.context
    2.17    val revert_abbrev: string -> string -> Proof.context -> Proof.context
    2.18    val verbose: bool ref
    2.19    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
    2.20 @@ -248,19 +249,20 @@
    2.21  
    2.22  val naming_of = #naming o rep_context;
    2.23  
    2.24 -fun name_decl decl (binding, x) ctxt =
    2.25 +fun name_decl decl (b, x) ctxt =
    2.26    let
    2.27      val naming = naming_of ctxt;
    2.28 -    val (naming', name) = Name.namify naming binding;
    2.29 +    val (naming', name) = Name.namify naming b;
    2.30    in
    2.31      ctxt
    2.32      |> map_naming (K naming')
    2.33 -    |> decl (Name.name_of binding, x)
    2.34 +    |> decl (Name.name_of b, x)
    2.35      |>> pair name
    2.36      ||> map_naming (K naming)
    2.37    end;
    2.38  
    2.39  val full_name = NameSpace.full o naming_of;
    2.40 +val full_binding = NameSpace.full_binding o naming_of;
    2.41  
    2.42  val syntax_of = #syntax o rep_context;
    2.43  val syn_of = LocalSyntax.syn_of o syntax_of;
    2.44 @@ -977,15 +979,14 @@
    2.45  
    2.46  local
    2.47  
    2.48 -fun update_thms _ (bname, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt bname))
    2.49 -  | update_thms do_props (bname, SOME ths) ctxt = ctxt |> map_facts
    2.50 -      (Facts.add_local do_props (naming_of ctxt) (full_name ctxt bname, ths));
    2.51 +fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_binding ctxt b))
    2.52 +  | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
    2.53 +      (Facts.add_local do_props (naming_of ctxt) (full_binding ctxt b, ths));
    2.54  
    2.55 -fun gen_note_thmss get k = fold_map (fn ((binding, more_attrs), raw_facts) => fn ctxt =>
    2.56 +fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
    2.57    let
    2.58 -    val bname = Name.name_of binding;
    2.59 -    val pos = Name.pos_of binding;
    2.60 -    val name = full_name ctxt bname;
    2.61 +    val pos = Name.pos_of b;
    2.62 +    val name = full_binding ctxt b;
    2.63      val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
    2.64  
    2.65      val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
    2.66 @@ -994,7 +995,7 @@
    2.67      val (res, ctxt') = fold_map app facts ctxt;
    2.68      val thms = PureThy.name_thms false false pos name (flat res);
    2.69      val Mode {stmt, ...} = get_mode ctxt;
    2.70 -  in ((name, thms), ctxt' |> update_thms stmt (bname, SOME thms)) end);
    2.71 +  in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
    2.72  
    2.73  in
    2.74  
    2.75 @@ -1004,7 +1005,7 @@
    2.76  fun put_thms do_props thms ctxt = ctxt
    2.77    |> map_naming (K local_naming)
    2.78    |> ContextPosition.set_visible false
    2.79 -  |> update_thms do_props thms
    2.80 +  |> update_thms do_props (apfst Name.binding thms)
    2.81    |> ContextPosition.restore_visible ctxt
    2.82    |> restore_naming ctxt;
    2.83  
    2.84 @@ -1023,9 +1024,9 @@
    2.85  local
    2.86  
    2.87  fun prep_vars prep_typ internal =
    2.88 -  fold_map (fn (raw_binding, raw_T, raw_mx) => fn ctxt =>
    2.89 +  fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
    2.90      let
    2.91 -      val raw_x = Name.name_of raw_binding;
    2.92 +      val raw_x = Name.name_of raw_b;
    2.93        val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
    2.94        val _ = Syntax.is_identifier (no_skolem internal x) orelse
    2.95          error ("Illegal variable name: " ^ quote x);
    2.96 @@ -1034,7 +1035,7 @@
    2.97          if internal then T
    2.98          else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
    2.99        val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
   2.100 -      val var = (Name.map_name (K x) raw_binding, opt_T, mx);
   2.101 +      val var = (Name.map_name (K x) raw_b, opt_T, mx);
   2.102      in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end);
   2.103  
   2.104  in
   2.105 @@ -1105,13 +1106,13 @@
   2.106        in cert_term ctxt (Const (c, T)); T end;
   2.107    in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end;
   2.108  
   2.109 -fun add_abbrev mode tags (c, raw_t) ctxt =
   2.110 +fun add_abbrev mode tags (b, raw_t) ctxt =
   2.111    let
   2.112      val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
   2.113 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
   2.114 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b));
   2.115      val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
   2.116      val ((lhs, rhs), consts') = consts_of ctxt
   2.117 -      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (c, t);
   2.118 +      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);
   2.119    in
   2.120      ctxt
   2.121      |> (map_consts o apfst) (K consts')
   2.122 @@ -1140,8 +1141,8 @@
   2.123        ctxt'
   2.124        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
   2.125        |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
   2.126 -    val _ = (vars ~~ xs') |> List.app (fn ((binding, _, _), x') =>
   2.127 -      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of binding));
   2.128 +    val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
   2.129 +      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of b));
   2.130    in (xs', ctxt'') end;
   2.131  
   2.132  in

     3.1 --- a/src/Pure/Isar/theory_target.ML	Thu Nov 20 14:51:40 2008 +0100
     3.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Nov 20 14:55:25 2008 +0100
     3.3 @@ -1,5 +1,6 @@
     3.4  (*  Title:      Pure/Isar/theory_target.ML
     3.5      ID:         $Id$
     3.6 +    ID:         $Id$
     3.7      Author:     Makarius
     3.8  
     3.9  Common theory/locale/class/instantiation/overloading targets.
    3.10 @@ -192,18 +193,18 @@
    3.11    else if not is_class then (NoSyn, mx, NoSyn)
    3.12    else (mx, NoSyn, NoSyn);
    3.13  
    3.14 -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi =
    3.15 +fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((b, mx), rhs) phi =
    3.16    let
    3.17 -    val c' = Morphism.name phi c;
    3.18 +    val b' = Morphism.name phi b;
    3.19      val rhs' = Morphism.term phi rhs;
    3.20 -    val name' = Name.name_with_prefix c';
    3.21 -    val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
    3.22 -    val arg = (name', Term.close_schematic_term rhs');
    3.23 +    val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
    3.24 +    val arg = (b', Term.close_schematic_term rhs');
    3.25      val similar_body = Type.similar_types (rhs, rhs');
    3.26      (* FIXME workaround based on educated guess *)
    3.27 -    val class_global = Name.name_of c = Name.name_of c'
    3.28 -      andalso not (null (Name.prefix_of c'))
    3.29 -      andalso (fst o snd o split_last) (Name.prefix_of c') = Class.class_prefix target;
    3.30 +    val (prefix', _) = Name.dest_binding b';
    3.31 +    val class_global = Name.name_of b = Name.name_of b'
    3.32 +      andalso not (null prefix')
    3.33 +      andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
    3.34    in
    3.35      not (is_class andalso (similar_body orelse class_global)) ?
    3.36        (Context.mapping_result
    3.37 @@ -267,7 +268,7 @@
    3.38    in
    3.39      lthy |>
    3.40       (if is_locale then
    3.41 -        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (c, global_rhs))
    3.42 +        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (b, global_rhs))
    3.43          #-> (fn (lhs, _) =>
    3.44            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    3.45              term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
    3.46 @@ -275,9 +276,9 @@
    3.47            end)
    3.48        else
    3.49          LocalTheory.theory
    3.50 -          (Sign.add_abbrev (#1 prmode) tags (c, global_rhs) #-> (fn (lhs, _) =>
    3.51 +          (Sign.add_abbrev (#1 prmode) tags (b, global_rhs) #-> (fn (lhs, _) =>
    3.52             Sign.notation true prmode [(lhs, mx3)])))
    3.53 -    |> ProofContext.add_abbrev PrintMode.internal tags (c, t) |> snd
    3.54 +    |> ProofContext.add_abbrev PrintMode.internal tags (b, t) |> snd
    3.55      |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
    3.56    end;
    3.57  

     4.1 --- a/src/Pure/consts.ML	Thu Nov 20 14:51:40 2008 +0100
     4.2 +++ b/src/Pure/consts.ML	Thu Nov 20 14:55:25 2008 +0100
     4.3 @@ -30,10 +30,10 @@
     4.4    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
     4.5    val typargs: T -> string * typ -> typ list
     4.6    val instance: T -> string * typ list -> typ
     4.7 -  val declare: bool -> NameSpace.naming -> Properties.T -> (bstring * typ) -> T -> T
     4.8 +  val declare: bool -> NameSpace.naming -> Properties.T -> (Name.binding * typ) -> T -> T
     4.9    val constrain: string * typ option -> T -> T
    4.10    val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
    4.11 -    bstring * term -> T -> (term * term) * T
    4.12 +    Name.binding * term -> T -> (term * term) * T
    4.13    val revert_abbrev: string -> string -> T -> T
    4.14    val hide: bool -> string -> T -> T
    4.15    val empty: T
    4.16 @@ -211,7 +211,7 @@
    4.17  fun err_dup_const c =
    4.18    error ("Duplicate declaration of constant " ^ quote c);
    4.19  
    4.20 -fun extend_decls naming decl tab = NameSpace.extend_table naming [decl] tab
    4.21 +fun extend_decls naming decl tab = NameSpace.table_declare naming decl tab
    4.22    handle Symtab.DUP c => err_dup_const c;
    4.23  
    4.24  
    4.25 @@ -223,11 +223,11 @@
    4.26  
    4.27  (* declarations *)
    4.28  
    4.29 -fun declare authentic naming tags (c, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
    4.30 +fun declare authentic naming tags (b, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
    4.31    let
    4.32      val tags' = tags |> Position.default_properties (Position.thread_data ());
    4.33      val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
    4.34 -    val decls' = decls |> extend_decls naming (c, ((decl, NONE), serial ()));
    4.35 +    val (_, decls') = decls |> extend_decls naming (b, ((decl, NONE), serial ()));
    4.36    in (decls', constraints, rev_abbrevs) end);
    4.37  
    4.38  
    4.39 @@ -262,7 +262,7 @@
    4.40  
    4.41  in
    4.42  
    4.43 -fun abbreviate pp tsig naming mode tags (c, raw_rhs) consts =
    4.44 +fun abbreviate pp tsig naming mode tags (b, raw_rhs) consts =
    4.45    let
    4.46      val cert_term = certify pp tsig false consts;
    4.47      val expand_term = certify pp tsig true consts;
    4.48 @@ -273,7 +273,7 @@
    4.49        |> cert_term;
    4.50      val normal_rhs = expand_term rhs;
    4.51      val T = Term.fastype_of rhs;
    4.52 -    val lhs = Const (NameSpace.full naming c, T);
    4.53 +    val lhs = Const (NameSpace.full_binding naming b, T);
    4.54  
    4.55      fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
    4.56        Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));
    4.57 @@ -285,8 +285,8 @@
    4.58          val tags' = tags |> Position.default_properties (Position.thread_data ());
    4.59          val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
    4.60          val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
    4.61 -        val decls' = decls
    4.62 -          |> extend_decls naming (c, ((decl, SOME abbr), serial ()));
    4.63 +        val (_, decls') = decls
    4.64 +          |> extend_decls naming (b, ((decl, SOME abbr), serial ()));
    4.65          val rev_abbrevs' = rev_abbrevs
    4.66            |> fold (curry Symtab.cons_list mode) (rev_abbrev lhs rhs);
    4.67        in (decls', constraints, rev_abbrevs') end)

     5.1 --- a/src/Pure/pure_thy.ML	Thu Nov 20 14:51:40 2008 +0100
     5.2 +++ b/src/Pure/pure_thy.ML	Thu Nov 20 14:55:25 2008 +0100
     5.3 @@ -143,35 +143,36 @@
     5.4  fun enter_proofs (thy, thms) =
     5.5    (FactsData.map (apsnd (fold (cons o lazy_proof) thms)) thy, thms);
     5.6  
     5.7 -fun enter_thms _ _ app_att ("", thms) thy = swap (enter_proofs (app_att (thy, thms)))
     5.8 -  | enter_thms pre_name post_name app_att (bname, thms) thy =
     5.9 -      let
    5.10 -        val naming = Sign.naming_of thy;
    5.11 -        val name = NameSpace.full naming bname;
    5.12 -        val (thy', thms') =
    5.13 -          enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
    5.14 -        val thms'' = map (Thm.transfer thy') thms';
    5.15 -        val thy'' = thy' |> FactsData.map (apfst (Facts.add_global naming (name, thms'')));
    5.16 -      in (thms'', thy'') end;
    5.17 +fun enter_thms pre_name post_name app_att (b, thms) thy =
    5.18 +  if Name.is_nothing b
    5.19 +  then swap (enter_proofs (app_att (thy, thms)))
    5.20 +  else let
    5.21 +    val naming = Sign.naming_of thy;
    5.22 +    val name = NameSpace.full_binding naming b;
    5.23 +    val (thy', thms') =
    5.24 +      enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
    5.25 +    val thms'' = map (Thm.transfer thy') thms';
    5.26 +    val thy'' = thy' |> FactsData.map (apfst (Facts.add_global naming (name, thms'')));
    5.27 +  in (thms'', thy'') end;
    5.28  
    5.29  
    5.30  (* store_thm(s) *)
    5.31  
    5.32 -val store_thms =
    5.33 -  enter_thms (name_thms true true Position.none) (name_thms false true Position.none) I;
    5.34 +fun store_thms (bname, thms) = enter_thms (name_thms true true Position.none)
    5.35 +  (name_thms false true Position.none) I (Name.binding bname, thms);
    5.36  
    5.37 -fun store_thm (name, th) = store_thms (name, [th]) #>> the_single;
    5.38 +fun store_thm (bname, th) = store_thms (bname, [th]) #>> the_single;
    5.39  
    5.40 -fun store_thm_open (name, th) =
    5.41 +fun store_thm_open (bname, th) =
    5.42    enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I
    5.43 -    (name, [th]) #>> the_single;
    5.44 +    (Name.binding bname, [th]) #>> the_single;
    5.45  
    5.46  
    5.47  (* add_thms(s) *)
    5.48  
    5.49  fun add_thms_atts pre_name ((bname, thms), atts) =
    5.50    enter_thms pre_name (name_thms false true Position.none)
    5.51 -    (foldl_map (Thm.theory_attributes atts)) (bname, thms);
    5.52 +    (foldl_map (Thm.theory_attributes atts)) (Name.binding bname, thms);
    5.53  
    5.54  fun gen_add_thmss pre_name =
    5.55    fold_map (add_thms_atts pre_name);
    5.56 @@ -195,17 +196,16 @@
    5.57  
    5.58  local
    5.59  
    5.60 -fun gen_note_thmss tag = fold_map (fn ((binding, more_atts), ths_atts) => fn thy =>
    5.61 +fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
    5.62    let
    5.63 -    val bname = Name.name_of binding;
    5.64 -    val pos = Name.pos_of binding;
    5.65 -    val name = Sign.full_name thy bname;
    5.66 +    val pos = Name.pos_of b;
    5.67 +    val name = Sign.full_binding thy b;
    5.68      val _ = Position.report (Markup.fact_decl name) pos;
    5.69  
    5.70      fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
    5.71      val (thms, thy') = thy |> enter_thms
    5.72        (name_thmss true pos) (name_thms false true pos) (apsnd flat o foldl_map app)
    5.73 -      (bname, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts);
    5.74 +      (b, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts);
    5.75    in ((name, thms), thy') end);
    5.76  
    5.77  in

     6.1 --- a/src/Pure/sign.ML	Thu Nov 20 14:51:40 2008 +0100
     6.2 +++ b/src/Pure/sign.ML	Thu Nov 20 14:55:25 2008 +0100
     6.3 @@ -18,6 +18,7 @@
     6.4    val name_decl: (string * 'a -> theory -> 'b * theory)
     6.5      -> Name.binding * 'a -> theory -> (string * 'b) * theory
     6.6    val full_name: theory -> bstring -> string
     6.7 +  val full_binding: theory -> Name.binding -> string
     6.8    val full_name_path: theory -> string -> bstring -> string
     6.9    val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
    6.10    val syn_of: theory -> Syntax.syntax
    6.11 @@ -93,10 +94,10 @@
    6.12    val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
    6.13    val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
    6.14    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
    6.15 +  val declare_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
    6.16    val add_consts: (bstring * string * mixfix) list -> theory -> theory
    6.17    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    6.18 -  val declare_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
    6.19 -  val add_abbrev: string -> Properties.T -> bstring * term -> theory -> (term * term) * theory
    6.20 +  val add_abbrev: string -> Properties.T -> Name.binding * term -> theory -> (term * term) * theory
    6.21    val revert_abbrev: string -> string -> theory -> theory
    6.22    val add_const_constraint: string * typ option -> theory -> theory
    6.23    val primitive_class: string * class list -> theory -> theory
    6.24 @@ -190,20 +191,21 @@
    6.25  val naming_of = #naming o rep_sg;
    6.26  val base_name = NameSpace.base;
    6.27  
    6.28 -fun name_decl decl (binding, x) thy =
    6.29 +fun name_decl decl (b, x) thy =
    6.30    let
    6.31      val naming = naming_of thy;
    6.32 -    val (naming', name) = Name.namify naming binding;
    6.33 +    val (naming', name) = Name.namify naming b;
    6.34    in
    6.35      thy
    6.36      |> map_naming (K naming')
    6.37 -    |> decl (Name.name_of binding, x)
    6.38 +    |> decl (Name.name_of b, x)
    6.39      |>> pair name
    6.40      ||> map_naming (K naming)
    6.41    end;
    6.42  
    6.43  val namify = Name.namify o naming_of;
    6.44  val full_name = NameSpace.full o naming_of;
    6.45 +val full_binding = NameSpace.full_binding o naming_of;
    6.46  fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));
    6.47  val declare_name = NameSpace.declare o naming_of;
    6.48  
    6.49 @@ -520,15 +522,16 @@
    6.50    let
    6.51      val ctxt = ProofContext.init thy;
    6.52      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    6.53 -    fun prep (raw_c, raw_T, raw_mx) =
    6.54 +    fun prep (raw_b, raw_T, raw_mx) =
    6.55        let
    6.56 -        val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
    6.57 -        val full_c = full_name thy c;
    6.58 -        val c' = if authentic then Syntax.constN ^ full_c else c;
    6.59 +        val (mx_name, mx) = Syntax.const_mixfix (Name.name_of raw_b) raw_mx;
    6.60 +        val b = Name.map_name (K mx_name) raw_b;
    6.61 +        val c = full_binding thy b;
    6.62 +        val c_syn = if authentic then Syntax.constN ^ c else Name.name_of b;
    6.63          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    6.64 -          cat_error msg ("in declaration of constant " ^ quote c);
    6.65 +          cat_error msg ("in declaration of constant " ^ quote (Name.display b));
    6.66          val T' = Logic.varifyT T;
    6.67 -      in ((c, T'), (c', T', mx), Const (full_c, T)) end;
    6.68 +      in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
    6.69      val args = map prep raw_args;
    6.70      val tags' = tags |> Properties.put (Markup.theory_nameN, Context.theory_name thy);
    6.71    in
    6.72 @@ -538,18 +541,19 @@
    6.73      |> pair (map #3 args)
    6.74    end;
    6.75  
    6.76 +fun bindify (name, T, mx) = (Name.binding name, T, mx);
    6.77 +
    6.78  in
    6.79  
    6.80 -val add_consts = snd oo gen_add_consts Syntax.parse_typ false [];
    6.81 -val add_consts_i = snd oo gen_add_consts (K I) false [];
    6.82 +fun add_consts args = snd o gen_add_consts Syntax.parse_typ false [] (map bindify args);
    6.83 +fun add_consts_i args = snd o gen_add_consts (K I) false [] (map bindify args);
    6.84  
    6.85  fun declare_const tags ((b, T), mx) thy =
    6.86    let
    6.87 -    val c = Name.name_of b;
    6.88      val pos = Name.pos_of b;
    6.89      val tags' = Position.default_properties pos tags;
    6.90 -    val ([const as Const (full_c, _)], thy') = gen_add_consts (K I) true tags' [(c, T, mx)] thy;
    6.91 -    val _ = Position.report (Markup.const_decl full_c) pos;
    6.92 +    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy;
    6.93 +    val _ = Position.report (Markup.const_decl c) pos;
    6.94    in (const, thy') end;
    6.95  
    6.96  end;
    6.97 @@ -557,14 +561,14 @@
    6.98  
    6.99  (* abbreviations *)
   6.100  
   6.101 -fun add_abbrev mode tags (c, raw_t) thy =
   6.102 +fun add_abbrev mode tags (b, raw_t) thy =
   6.103    let
   6.104      val pp = Syntax.pp_global thy;
   6.105      val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
   6.106      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
   6.107 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
   6.108 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b));
   6.109      val (res, consts') = consts_of thy
   6.110 -      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (c, t);
   6.111 +      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
   6.112    in (res, thy |> map_consts (K consts')) end;
   6.113  
   6.114  fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);