# HG changeset patch
# User wenzelm
# Date 1236460610 -3600
# Node ID 10a67c5ddddb8b544c44208c0b6675d92864f8a3
# Parent  79f022df8527f2ce02b0f293693597143f40745b
more uniform handling of binding in targets and derived elements;

diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/class.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -10,9 +10,9 @@
     (*FIXME the split into class_target.ML, theory_target.ML and
       class.ML is artificial*)
 
-  val class: bstring -> class list -> Element.context_i list
+  val class: binding -> class list -> Element.context_i list
     -> theory -> string * local_theory
-  val class_cmd: bstring -> xstring list -> Element.context list
+  val class_cmd: binding -> xstring list -> Element.context list
     -> theory -> string * local_theory
   val prove_subclass: tactic -> class -> local_theory -> local_theory
   val subclass: class -> local_theory -> Proof.state
@@ -73,7 +73,7 @@
     val morph = base_morph $> eq_morph;
 
     (* assm_intro *)
-    fun prove_assm_intro thm = 
+    fun prove_assm_intro thm =
       let
         val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt;
         val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
@@ -169,7 +169,7 @@
     val _ = case filter_out (is_class thy) sups
      of [] => ()
       | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
-          val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
+    val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
     val supparam_names = map fst supparams;
     val _ = if has_duplicates (op =) supparam_names
       then error ("Duplicate parameter(s) in superclasses: "
@@ -200,7 +200,7 @@
       | check_element e = [()];
     val _ = map check_element syntax_elems;
     fun fork_syn (Element.Fixes xs) =
-          fold_map (fn (c, ty, syn) => cons (Binding.name_of c, syn) #> pair (c, ty, NoSyn)) xs
+          fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
           #>> Element.Fixes
       | fork_syn x = pair x;
     val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
@@ -217,7 +217,7 @@
 
 (* class establishment *)
 
-fun add_consts bname class base_sort sups supparams global_syntax thy =
+fun add_consts class base_sort sups supparams global_syntax thy =
   let
     (*FIXME simplify*)
     val supconsts = supparams
@@ -227,17 +227,16 @@
     val raw_params = (snd o chop (length supparams)) all_params;
     fun add_const (b, SOME raw_ty, _) thy =
       let
-        val v = Binding.name_of b;
-        val c = Sign.full_bname thy v;
+        val c = Sign.full_name thy b;
         val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
         val ty0 = Type.strip_sorts ty;
         val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
-        val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v;
+        val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
       in
         thy
-        |> Sign.declare_const [] ((Binding.name v, ty0), syn)
+        |> Sign.declare_const [] ((b, ty0), syn)
         |> snd
-        |> pair ((v, ty), (c, ty'))
+        |> pair ((Binding.name_of b, ty), (c, ty'))
       end;
   in
     thy
@@ -261,7 +260,7 @@
       | [thm] => SOME thm;
   in
     thy
-    |> add_consts bname class base_sort sups supparams global_syntax
+    |> add_consts class base_sort sups supparams global_syntax
     |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
           (map (fst o snd) params)
           [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
@@ -273,12 +272,12 @@
 
 fun gen_class prep_spec bname raw_supclasses raw_elems thy =
   let
-    val class = Sign.full_bname thy bname;
+    val class = Sign.full_name thy bname;
     val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
       prep_spec thy raw_supclasses raw_elems;
   in
     thy
-    |> Expression.add_locale bname "" supexpr elems
+    |> Expression.add_locale bname Binding.empty supexpr elems
     |> snd |> LocalTheory.exit_global
     |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
     |-> (fn (param_map, params, assm_axiom) =>
diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -24,9 +24,9 @@
   val begin: class list -> sort -> Proof.context -> Proof.context
   val init: class -> theory -> Proof.context
   val declare: class -> Properties.T
-    -> (string * mixfix) * term -> theory -> theory
+    -> (binding * mixfix) * term -> theory -> theory
   val abbrev: class -> Syntax.mode -> Properties.T
-    -> (string * mixfix) * term -> theory -> theory
+    -> (binding * mixfix) * term -> theory -> theory
   val class_prefix: string -> string
   val refresh_syntax: class -> Proof.context -> Proof.context
   val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
@@ -52,12 +52,12 @@
   val default_intro_tac: Proof.context -> thm list -> tactic
 
   (*old axclass layer*)
-  val axclass_cmd: bstring * xstring list
+  val axclass_cmd: binding * xstring list
     -> (Attrib.binding * string list) list
     -> theory -> class * theory
   val classrel_cmd: xstring * xstring -> theory -> Proof.state
   val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
-  val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
+  val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
 end;
 
 structure Class_Target : CLASS_TARGET =
@@ -363,8 +363,8 @@
 fun declare class pos ((c, mx), dict) thy =
   let
     val morph = morphism thy class;
-    val b = Morphism.binding morph (Binding.name c);
-    val b_def = Morphism.binding morph (Binding.name (c ^ "_dict"));
+    val b = Morphism.binding morph c;
+    val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b);
     val c' = Sign.full_name thy b;
     val dict' = Morphism.term morph dict;
     val ty' = Term.fastype_of dict';
@@ -386,7 +386,7 @@
   let
     val morph = morphism thy class;
     val unchecks = these_unchecks thy [class];
-    val b = Morphism.binding morph (Binding.name c);
+    val b = Morphism.binding morph c;
     val c' = Sign.full_name thy b;
     val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
     val ty' = Term.fastype_of rhs';
diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -44,13 +44,13 @@
           else ());
 
     val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
-    val name = Thm.def_name_optional c (Binding.name_of raw_name);
+    val name = Binding.map_name (Thm.def_name_optional c) raw_name;
     val atts = map (prep_att thy) raw_atts;
 
     val thy' =
       thy
-      |> Sign.add_consts_i [(c, T, mx)]
-      |> PureThy.add_defs false [((Binding.name name, def), atts)]
+      |> Sign.add_consts_i [(Binding.name c, T, mx)]
+      |> PureThy.add_defs false [((name, def), atts)]
       |-> (fn [thm] => Code.add_default_eqn thm);
   in ((c, T), thy') end;
 
diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -29,9 +29,9 @@
   val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
     Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
       * Element.context_i list) * ((string * typ) list * Proof.context)
-  val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
+  val add_locale: binding -> binding -> expression_i -> Element.context_i list ->
     theory -> string * local_theory
-  val add_locale_cmd: bstring -> bstring -> expression -> Element.context list ->
+  val add_locale_cmd: binding -> binding -> expression -> Element.context list ->
     theory -> string * local_theory
 
   (* Interpretation *)
@@ -41,15 +41,12 @@
     (term list list * (string * morphism) list * morphism) * Proof.context
   val sublocale: string -> expression_i -> theory -> Proof.state
   val sublocale_cmd: string -> expression -> theory -> Proof.state
-  val interpretation: expression_i -> (Attrib.binding * term) list ->
-    theory -> Proof.state
-  val interpretation_cmd: expression -> (Attrib.binding * string) list ->
-    theory -> Proof.state
+  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
+  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
   val interpret: expression_i -> bool -> Proof.state -> Proof.state
   val interpret_cmd: expression -> bool -> Proof.state -> Proof.state
 end;
 
-
 structure Expression : EXPRESSION =
 struct
 
@@ -90,11 +87,10 @@
 
     fun match_bind (n, b) = (n = Binding.name_of b);
     fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
-      (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *)
-      Binding.name_of b1 = Binding.name_of b2 andalso
+      Binding.eq_name (b1, b2) andalso
         (mx1 = mx2 orelse
           error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
-      
+
     fun params_loc loc =
       (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
     fun params_inst (expr as (loc, (prfx, Positional insts))) =
@@ -132,8 +128,10 @@
     val implicit' = map (#1 #> Binding.name_of) implicit;
     val fixed' = map (#1 #> Binding.name_of) fixed;
     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
-    val implicit'' = if strict then []
-      else let val _ = reject_dups
+    val implicit'' =
+      if strict then []
+      else
+        let val _ = reject_dups
           "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed')
         in map (fn (b, mx) => (b, NONE, mx)) implicit end;
 
@@ -176,7 +174,7 @@
     val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
     val res = Syntax.check_terms ctxt arg;
     val ctxt' = ctxt |> fold Variable.auto_fixes res;
-    
+
     (* instantiation *)
     val (type_parms'', res') = chop (length type_parms) res;
     val insts'' = (parm_names ~~ res') |> map_filter
@@ -330,7 +328,7 @@
   let
     val elem' = finish_primitive parms (closeup ctxt parms do_close) elem;
   in elem' end
-  
+
 fun finish ctxt parms do_close insts elems =
   let
     val deps = map (finish_inst ctxt parms do_close) insts;
@@ -366,7 +364,7 @@
         val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
         val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt;
       in (i+1, insts', ctxt'') end;
-  
+
     fun prep_elem insts raw_elem (elems, ctxt) =
       let
         val ctxt' = declare_elem prep_vars_elem raw_elem ctxt;
@@ -390,7 +388,7 @@
     (* Retrieve parameter types *)
     val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.name_of o #1) fixes)
       | _ => fn ps => ps) (Fixes fors :: elems') [];
-    val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6; 
+    val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6;
     val parms = xs ~~ Ts;  (* params from expression and elements *)
 
     val Fixes fors' = finish_primitive parms I (Fixes fors);
@@ -490,7 +488,7 @@
     val exp_typ = Logic.type_map exp_term;
     val export' = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
   in ((propss, deps, export'), goal_ctxt) end;
-    
+
 in
 
 fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x;
@@ -617,7 +615,7 @@
 
 fun def_pred bname parms defs ts norm_ts thy =
   let
-    val name = Sign.full_bname thy bname;
+    val name = Sign.full_name thy bname;
 
     val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
     val env = Term.add_free_names body [];
@@ -635,9 +633,9 @@
     val ([pred_def], defs_thy) =
       thy
       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
-      |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd
+      |> Sign.declare_const [] ((bname, predT), NoSyn) |> snd
       |> PureThy.add_defs false
-        [((Binding.name (Thm.def_name bname), Logic.mk_equals (head, body)), [Thm.kind_internal])];
+        [((Binding.map_name Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
 
     val cert = Thm.cterm_of defs_thy;
@@ -660,7 +658,7 @@
 
 in
 
-(* CB: main predicate definition function *)
+(* main predicate definition function *)
 
 fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy =
   let
@@ -670,13 +668,13 @@
       if null exts then (NONE, NONE, [], thy)
       else
         let
-          val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
+          val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname
           val ((statement, intro, axioms), thy') =
             thy
             |> def_pred aname parms defs' exts exts';
           val (_, thy'') =
             thy'
-            |> Sign.add_path aname
+            |> Sign.add_path (Binding.name_of aname)
             |> Sign.no_base_names
             |> PureThy.note_thmss Thm.internalK
               [((Binding.name introN, []), [([intro], [Locale.unfold_attrib])])]
@@ -691,7 +689,7 @@
             |> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
           val (_, thy'''') =
             thy'''
-            |> Sign.add_path pname
+            |> Sign.add_path (Binding.name_of pname)
             |> Sign.no_base_names
             |> PureThy.note_thmss Thm.internalK
                  [((Binding.name introN, []), [([intro], [Locale.intro_attrib])]),
@@ -722,7 +720,7 @@
 fun gen_add_locale prep_decl
     bname raw_predicate_bname raw_import raw_body thy =
   let
-    val name = Sign.full_bname thy bname;
+    val name = Sign.full_name thy bname;
     val _ = Locale.defined thy name andalso
       error ("Duplicate definition of locale " ^ quote name);
 
@@ -730,14 +728,16 @@
       prep_decl raw_import I raw_body (ProofContext.init thy);
     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
 
-    val predicate_bname = if raw_predicate_bname = "" then bname
+    val predicate_bname =
+      if Binding.is_empty raw_predicate_bname then bname
       else raw_predicate_bname;
     val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
       define_preds predicate_bname parms text thy;
 
     val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
-    val _ = if null extraTs then ()
-      else warning ("Additional type variable(s) in locale specification " ^ quote bname);
+    val _ =
+      if null extraTs then ()
+      else warning ("Additional type variable(s) in locale specification " ^ quote (Binding.str_of bname));
 
     val a_satisfy = Element.satisfy_morphism a_axioms;
     val b_satisfy = Element.satisfy_morphism b_axioms;
@@ -748,7 +748,7 @@
 
     val notes =
         if is_some asm
-        then [(Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
+        then [(Thm.internalK, [((Binding.suffix_name ("_" ^ axiomsN) bname, []),
           [([Assumption.assume (cterm_of thy' (the asm))],
             [(Attrib.internal o K) Locale.witness_attrib])])])]
         else [];
@@ -766,7 +766,7 @@
 
     val loc_ctxt = thy'
       |> Locale.register_locale bname (extraTs, params)
-          (asm, rev defs) (a_intro, b_intro) axioms ([], []) 
+          (asm, rev defs) (a_intro, b_intro) axioms ([], [])
           (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev)
       |> TheoryTarget.init (SOME name)
       |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
@@ -793,7 +793,7 @@
     val target_ctxt = Locale.init target thy;
 
     val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
-    
+
     fun after_qed witss = ProofContext.theory (
       fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
         (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
@@ -879,7 +879,7 @@
     val ctxt = Proof.context_of state;
 
     val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
-    
+
     fun store_reg (name, morph) thms =
       let
         val morph' = morph $> Element.satisfy_morphism thms $> export;
diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -86,7 +86,7 @@
 
 val _ =
   OuterSyntax.command "classes" "declare type classes" K.thy_decl
-    (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
+    (Scan.repeat1 (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
         P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
 
 val _ =
@@ -100,7 +100,7 @@
 
 val _ =
   OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
-    (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
+    (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
         P.!!! (P.list1 P.xname)) []
         -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
       >> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y)));
@@ -110,19 +110,19 @@
 
 val _ =
   OuterSyntax.command "typedecl" "type declaration" K.thy_decl
-    (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
+    (P.type_args -- P.binding -- P.opt_infix >> (fn ((args, a), mx) =>
       Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd)));
 
 val _ =
   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
     (Scan.repeat1
-      (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
+      (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
       >> (Toplevel.theory o Sign.add_tyabbrs o
         map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
 
 val _ =
   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
-    K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Sign.add_nonterminals));
+    K.thy_decl (Scan.repeat1 P.binding >> (Toplevel.theory o Sign.add_nonterminals));
 
 val _ =
   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
@@ -133,11 +133,11 @@
 
 val _ =
   OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
-    (P.const >> (Toplevel.theory o ObjectLogic.add_judgment));
+    (P.const_binding >> (Toplevel.theory o ObjectLogic.add_judgment_cmd));
 
 val _ =
   OuterSyntax.command "consts" "declare constants" K.thy_decl
-    (Scan.repeat1 P.const >> (Toplevel.theory o Sign.add_consts));
+    (Scan.repeat1 P.const_binding >> (Toplevel.theory o Sign.add_consts));
 
 val opt_overloaded = P.opt_keyword "overloaded";
 
@@ -392,10 +392,10 @@
 
 val _ =
   OuterSyntax.command "locale" "define named proof context" K.thy_decl
-    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
+    (P.binding -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-            (Expression.add_locale_cmd name "" expr elems #> snd)));
+            (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
 
 val _ =
   OuterSyntax.command "sublocale"
@@ -430,7 +430,7 @@
 
 val _ =
   OuterSyntax.command "class" "define type class" K.thy_decl
-   (P.name -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin
+   (P.binding -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
         (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
           (Class.class_cmd name supclasses elems #> snd)));
diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -30,7 +30,7 @@
 signature LOCALE =
 sig
   (* Locale specification *)
-  val register_locale: bstring ->
+  val register_locale: binding ->
     (string * sort) list * (binding * typ option * mixfix) list ->
     term option * term list ->
     thm option * thm option -> thm list ->
@@ -78,7 +78,7 @@
 
   (* Diagnostic *)
   val print_locales: theory -> unit
-  val print_locale: theory -> bool -> bstring -> unit
+  val print_locale: theory -> bool -> xstring -> unit
 end;
 
 
@@ -173,8 +173,8 @@
  of SOME (Loc loc) => loc
   | NONE => error ("Unknown locale " ^ quote name);
 
-fun register_locale bname parameters spec intros axioms decls notes dependencies thy =
-  thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
+fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
+  thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (binding,
     mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies))) #> snd);
 
 fun change_locale name =
diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/object_logic.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -8,9 +8,9 @@
 sig
   val get_base_sort: theory -> sort option
   val add_base_sort: sort -> theory -> theory
-  val typedecl: bstring * string list * mixfix -> theory -> typ * theory
-  val add_judgment: bstring * string * mixfix -> theory -> theory
-  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
+  val typedecl: binding * string list * mixfix -> theory -> typ * theory
+  val add_judgment: binding * typ * mixfix -> theory -> theory
+  val add_judgment_cmd: binding * string * mixfix -> theory -> theory
   val judgment_name: theory -> string
   val is_judgment: theory -> term -> bool
   val drop_judgment: theory -> term -> term
@@ -85,17 +85,18 @@
 
 (* typedecl *)
 
-fun typedecl (raw_name, vs, mx) thy =
+fun typedecl (a, vs, mx) thy =
   let
     val base_sort = get_base_sort thy;
-    val name = Sign.full_bname thy (Syntax.type_name raw_name mx);
+    val b = Binding.map_name (Syntax.type_name mx) a;
     val _ = has_duplicates (op =) vs andalso
-      error ("Duplicate parameters in type declaration: " ^ quote name);
+      error ("Duplicate parameters in type declaration: " ^ quote (Binding.str_of b));
+    val name = Sign.full_name thy b;
     val n = length vs;
     val T = Type (name, map (fn v => TFree (v, [])) vs);
   in
     thy
-    |> Sign.add_types [(raw_name, n, mx)]
+    |> Sign.add_types [(a, n, mx)]
     |> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
     |> pair T
   end;
@@ -105,10 +106,10 @@
 
 local
 
-fun gen_add_judgment add_consts (bname, T, mx) thy =
-  let val c = Sign.full_bname thy (Syntax.const_name bname mx) in
+fun gen_add_judgment add_consts (b, T, mx) thy =
+  let val c = Sign.full_name thy (Binding.map_name (Syntax.const_name mx) b) in
     thy
-    |> add_consts [(bname, T, mx)]
+    |> add_consts [(b, T, mx)]
     |> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')
     |> map_data (fn (base_sort, judgment, atomize_rulify) =>
         if is_some judgment then error "Attempt to redeclare object-logic judgment"
@@ -117,8 +118,8 @@
 
 in
 
-val add_judgment = gen_add_judgment Sign.add_consts;
-val add_judgment_i = gen_add_judgment Sign.add_consts_i;
+val add_judgment = gen_add_judgment Sign.add_consts_i;
+val add_judgment_cmd = gen_add_judgment Sign.add_consts;
 
 end;
 
diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -181,7 +181,7 @@
                 Position.str_of (Binding.pos_of b));
           in (b, mx) end);
     val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
-        (var, ((Binding.map_name (suffix "_raw") name, []), rhs));
+        (var, ((Binding.suffix_name "_raw" name, []), rhs));
     val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
         ((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
 
diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -189,7 +189,7 @@
     val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
     val prefix' = Binding.prefix_of b';
-    val class_global = Binding.name_of b = Binding.name_of b'
+    val class_global = Binding.eq_name (b, b')
       andalso not (null prefix')
       andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
   in
@@ -210,7 +210,7 @@
 
 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   let
-    val c = Binding.name_of b;
+    val c = Binding.name_of b;  (* FIXME Binding.qualified_name_of *)
     val tags = LocalTheory.group_position_of lthy;
     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
     val U = map #2 xs ---> T;
@@ -233,7 +233,7 @@
   in
     lthy'
     |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((b, mx2), t))
-    |> is_class ? class_target ta (Class_Target.declare target tags ((c, mx1), t))
+    |> is_class ? class_target ta (Class_Target.declare target tags ((b, mx1), t))
     |> LocalDefs.add_def ((b, NoSyn), t)
   end;
 
@@ -242,7 +242,6 @@
 
 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   let
-    val c = Binding.name_of b;
     val tags = LocalTheory.group_position_of lthy;
     val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
     val target_ctxt = LocalTheory.target_of lthy;
@@ -260,7 +259,7 @@
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
             term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
-            is_class ? class_target ta (Class_Target.abbrev target prmode tags ((c, mx1), t'))
+            is_class ? class_target ta (Class_Target.abbrev target prmode tags ((b, mx1), t'))
           end)
       else
         LocalTheory.theory
@@ -279,8 +278,8 @@
     val thy = ProofContext.theory_of lthy;
     val thy_ctxt = ProofContext.init thy;
 
-    val c = Binding.name_of b;
-    val name' = Binding.map_name (Thm.def_name_optional c) name;
+    val c = Binding.name_of b;   (* FIXME Binding.qualified_name_of (!?) *)
+    val name' = Binding.map_name (Thm.def_name_optional (Binding.name_of b)) name;
     val (rhs', rhs_conv) =
       LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
     val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -37,12 +37,12 @@
   thy
   |> Theory.copy
   |> Sign.root_path
-  |> Sign.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
+  |> Sign.add_types [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
   |> Sign.add_consts
-      [("typeof", "'b::{} => Type", NoSyn),
-       ("Type", "'a::{} itself => Type", NoSyn),
-       ("Null", "Null", NoSyn),
-       ("realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
+      [(Binding.name "typeof", "'b::{} => Type", NoSyn),
+       (Binding.name "Type", "'a::{} itself => Type", NoSyn),
+       (Binding.name "Null", "Null", NoSyn),
+       (Binding.name "realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
 
 val nullT = Type ("Null", []);
 val nullt = Const ("Null", nullT);
@@ -732,7 +732,7 @@
              val fu = Type.freeze u;
              val (def_thms, thy') = if t = nullt then ([], thy) else
                thy
-               |> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
+               |> Sign.add_consts_i [(Binding.name (extr_name s vs), fastype_of ft, NoSyn)]
                |> PureThy.add_defs false [((Binding.name (extr_name s vs ^ "_def"),
                     Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
            in
diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -37,7 +37,7 @@
 fun add_proof_atom_consts names thy =
   thy
   |> Sign.absolute_path
-  |> Sign.add_consts_i (map (fn name => (name, proofT, NoSyn)) names);
+  |> Sign.add_consts_i (map (fn name => (Binding.name name, proofT, NoSyn)) names);
 
 (** constants for application and abstraction **)
 
@@ -46,16 +46,16 @@
   |> Theory.copy
   |> Sign.root_path
   |> Sign.add_defsort_i []
-  |> Sign.add_types [("proof", 0, NoSyn)]
+  |> Sign.add_types [(Binding.name "proof", 0, NoSyn)]
   |> Sign.add_consts_i
-      [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
-       ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
-       ("Abst", (aT --> proofT) --> proofT, NoSyn),
-       ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
-       ("Hyp", propT --> proofT, NoSyn),
-       ("Oracle", propT --> proofT, NoSyn),
-       ("MinProof", proofT, Delimfix "?")]
-  |> Sign.add_nonterminals ["param", "params"]
+      [(Binding.name "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
+       (Binding.name "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
+       (Binding.name "Abst", (aT --> proofT) --> proofT, NoSyn),
+       (Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
+       (Binding.name "Hyp", propT --> proofT, NoSyn),
+       (Binding.name "Oracle", propT --> proofT, NoSyn),
+       (Binding.name "MinProof", proofT, Delimfix "?")]
+  |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"]
   |> Sign.add_syntax_i
       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
        ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/axclass.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -7,7 +7,7 @@
 
 signature AX_CLASS =
 sig
-  val define_class: bstring * class list -> string list ->
+  val define_class: binding * class list -> string list ->
     (Thm.binding * term list) list -> theory -> class * theory
   val add_classrel: thm -> theory -> theory
   val add_arity: thm -> theory -> theory
@@ -19,8 +19,8 @@
   val class_of_param: theory -> string -> class option
   val cert_classrel: theory -> class * class -> class * class
   val read_classrel: theory -> xstring * xstring -> class * class
-  val axiomatize_class: bstring * class list -> theory -> theory
-  val axiomatize_class_cmd: bstring * xstring list -> theory -> theory
+  val axiomatize_class: binding * class list -> theory -> theory
+  val axiomatize_class_cmd: binding * xstring list -> theory -> theory
   val axiomatize_classrel: (class * class) list -> theory -> theory
   val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory
   val axiomatize_arity: arity -> theory -> theory
@@ -325,8 +325,7 @@
   let
     val ctxt = ProofContext.init thy;
     val (c1, c2) = cert_classrel thy raw_rel;
-    val th = Goal.prove ctxt [] []
-        (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg =>
+    val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
       cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
         quote (Syntax.string_of_classrel ctxt [c1, c2]));
   in
@@ -374,14 +373,15 @@
     |> Sign.sticky_prefix name_inst
     |> Sign.no_base_names
     |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
-    |-> (fn const' as Const (c'', _) => Thm.add_def false true
-          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
-    #>> Thm.varifyT
-    #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
-    #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal])
-    #> snd
-    #> Sign.restore_naming thy
-    #> pair (Const (c, T))))
+    |-> (fn const' as Const (c'', _) =>
+      Thm.add_def false true
+        (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
+      #>> Thm.varifyT
+      #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
+      #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal])
+      #> snd
+      #> Sign.restore_naming thy
+      #> pair (Const (c, T))))
   end;
 
 fun define_overloaded name (c, t) thy =
@@ -390,8 +390,7 @@
     val SOME tyco = inst_tyco_of thy (c, T);
     val (c', eq) = get_inst_param thy (c, tyco);
     val prop = Logic.mk_equals (Const (c', T), t);
-    val name' = Thm.def_name_optional
-      (NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco) name;
+    val name' = Thm.def_name_optional (NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco) name;
   in
     thy
     |> Thm.add_def false false (Binding.name name', prop)
@@ -424,8 +423,8 @@
 
     (* class *)
 
-    val bconst = Logic.const_of_class bclass;
-    val class = Sign.full_bname thy bclass;
+    val bconst = Binding.map_name Logic.const_of_class bclass;
+    val class = Sign.full_name thy bclass;
     val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super);
 
     fun check_constraint (a, S) =
@@ -472,7 +471,7 @@
     val ([def], def_thy) =
       thy
       |> Sign.primitive_class (bclass, super)
-      |> PureThy.add_defs false [((Binding.name (Thm.def_name bconst), class_eq), [])];
+      |> PureThy.add_defs false [((Binding.map_name Thm.def_name bconst, class_eq), [])];
     val (raw_intro, (raw_classrel, raw_axioms)) =
       split_defined (length conjs) def ||> chop (length super);
 
@@ -482,7 +481,7 @@
     val class_triv = Thm.class_triv def_thy class;
     val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
       def_thy
-      |> Sign.add_path bconst
+      |> Sign.add_path (Binding.name_of bconst)
       |> Sign.no_base_names
       |> PureThy.note_thmss ""
         [((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
@@ -498,7 +497,7 @@
     val result_thy =
       facts_thy
       |> fold put_classrel (map (pair class) super ~~ classrel)
-      |> Sign.add_path bconst
+      |> Sign.add_path (Binding.name_of bconst)
       |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
       |> Sign.restore_naming facts_thy
       |> map_axclasses (fn (axclasses, parameters) =>
@@ -537,7 +536,7 @@
 
 fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
   let
-    val class = Sign.full_bname thy bclass;
+    val class = Sign.full_name thy bclass;
     val super = map (prep_class thy) raw_super |> Sign.minimize_sort thy;
   in
     thy
diff -r 79f022df8527 -r 10a67c5ddddb src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/pure_thy.ML	Sat Mar 07 22:16:50 2009 +0100
@@ -290,11 +290,11 @@
 val _ = Context.>> (Context.map_theory
   (OldApplSyntax.init #>
    Sign.add_types
-   [("fun", 2, NoSyn),
-    ("prop", 0, NoSyn),
-    ("itself", 1, NoSyn),
-    ("dummy", 0, NoSyn)]
-  #> Sign.add_nonterminals Syntax.basic_nonterms
+   [(Binding.name "fun", 2, NoSyn),
+    (Binding.name "prop", 0, NoSyn),
+    (Binding.name "itself", 1, NoSyn),
+    (Binding.name "dummy", 0, NoSyn)]
+  #> Sign.add_nonterminals (map Binding.name Syntax.basic_nonterms)
   #> Sign.add_syntax_i
    [("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3%_./ _)", [0, 3], 3)),
     ("_abs",        typ "'a",                          NoSyn),
@@ -360,12 +360,12 @@
   #> Sign.add_modesyntax_i ("HTML", false)
    [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
   #> Sign.add_consts_i
-   [("==", typ "'a => 'a => prop", InfixrName ("==", 2)),
-    ("==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
-    ("all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
-    ("prop", typ "prop => prop", NoSyn),
-    ("TYPE", typ "'a itself", NoSyn),
-    (Term.dummy_patternN, typ "'a", Delimfix "'_")]
+   [(Binding.name "==", typ "'a => 'a => prop", InfixrName ("==", 2)),
+    (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
+    (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
+    (Binding.name "prop", typ "prop => prop", NoSyn),
+    (Binding.name "TYPE", typ "'a itself", NoSyn),
+    (Binding.name Term.dummy_patternN, typ "'a", Delimfix "'_")]
   #> Theory.add_deps "==" ("==", typ "'a => 'a => prop") []
   #> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") []
   #> Theory.add_deps "all" ("all", typ "('a => prop) => prop") []
@@ -375,9 +375,9 @@
   #> Sign.add_trfunsT Syntax.pure_trfunsT
   #> Sign.local_path
   #> Sign.add_consts_i
-   [("term", typ "'a => prop", NoSyn),
-    ("sort_constraint", typ "'a itself => prop", NoSyn),
-    ("conjunction", typ "prop => prop => prop", NoSyn)]
+   [(Binding.name "term", typ "'a => prop", NoSyn),
+    (Binding.name "sort_constraint", typ "'a itself => prop", NoSyn),
+    (Binding.name "conjunction", typ "prop => prop => prop", NoSyn)]
   #> (add_defs false o map Thm.no_attributes)
    [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
     (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),