# HG changeset patch
# User wenzelm
# Date 1236796068 -3600
# Node ID 53d6a1c110f152e91faed9f7f095505652a04ee4
# Parent  c816b6dcc8afb0d2932ef89fb1bb72f2e1bf9823# Parent  757ba2bb2b3973c52c3051255233cdbb7eed9499
merged

diff -r c816b6dcc8af -r 53d6a1c110f1 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -575,7 +575,7 @@
              Attrib.internal (K (RuleCases.consumes 1))]),
            strong_inducts) |> snd |>
         LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) =>
-            ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
+            ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
               [Attrib.internal (K (RuleCases.case_names (map snd cases))),
                Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
           (strong_cases ~~ induct_cases')) |> snd
@@ -665,7 +665,7 @@
   in
     ctxt |>
     LocalTheory.notes Thm.theoremK (map (fn (name, ths) =>
-        ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
+        ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
           [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
       (names ~~ transp thss)) |> snd
   end;
diff -r c816b6dcc8af -r 53d6a1c110f1 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -128,8 +128,9 @@
     val ind_name = Thm.get_name induction;
     val vs = map (fn i => List.nth (pnames, i)) is;
     val (thm', thy') = thy
-      |> Sign.absolute_path
-      |> PureThy.store_thm (Binding.name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
+      |> Sign.root_path
+      |> PureThy.store_thm
+        (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
       ||> Sign.restore_naming thy;
 
     val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
@@ -194,8 +195,8 @@
 
     val exh_name = Thm.get_name exhaustion;
     val (thm', thy') = thy
-      |> Sign.absolute_path
-      |> PureThy.store_thm (Binding.name (exh_name ^ "_P_correctness"), thm)
+      |> Sign.root_path
+      |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
       ||> Sign.restore_naming thy;
 
     val P = Var (("P", 0), rT' --> HOLogic.boolT);
diff -r c816b6dcc8af -r 53d6a1c110f1 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -1,10 +1,8 @@
 (*  Title:      HOL/Tools/function_package/fundef_package.ML
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
 A package for general recursive function definitions.
 Isar commands.
-
 *)
 
 signature FUNDEF_PACKAGE =
@@ -36,7 +34,8 @@
 open FundefLib
 open FundefCommon
 
-fun note_theorem ((name, atts), ths) = LocalTheory.note Thm.theoremK ((Binding.name name, atts), ths)
+fun note_theorem ((name, atts), ths) =
+  LocalTheory.note Thm.theoremK ((Binding.qualified_name name, atts), ths)
 
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
 
diff -r c816b6dcc8af -r 53d6a1c110f1 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -698,7 +698,7 @@
       ctxt1 |>
       LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>>
       fold_map (fn (name, (elim, cases)) =>
-        LocalTheory.note kind ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "cases"),
+        LocalTheory.note kind ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "cases"),
           [Attrib.internal (K (RuleCases.case_names cases)),
            Attrib.internal (K (RuleCases.consumes 1)),
            Attrib.internal (K (Induct.cases_pred name)),
diff -r c816b6dcc8af -r 53d6a1c110f1 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -355,7 +355,7 @@
           ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
            subst_atomic rlzpreds' (Logic.unvarify rintr)))
              (rintrs ~~ maps snd rss)) [] ||>
-      Sign.absolute_path;
+      Sign.root_path;
     val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
 
     (** realizer for induction rule **)
@@ -394,12 +394,12 @@
            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
              [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
-        val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
+        val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
           (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
         val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
           (DatatypeAux.split_conj_thm thm');
         val ([thms'], thy'') = PureThy.add_thmss
-          [((Binding.name (space_implode "_"
+          [((Binding.qualified_name (space_implode "_"
              (Long_Name.qualify qualifier "inducts" :: vs' @ Ps @
                ["correctness"])), thms), [])] thy';
         val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
@@ -454,7 +454,7 @@
            rewrite_goals_tac rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
-        val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
+        val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
           (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
       in
         Extraction.add_realizers_i
diff -r c816b6dcc8af -r 53d6a1c110f1 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -259,7 +259,7 @@
     |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
     |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
     |-> (fn simps' => LocalTheory.note Thm.theoremK
-          ((qualify (Binding.name "simps"), simp_atts), maps snd simps'))
+          ((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps'))
     |>> snd
   end handle PrimrecError (msg, some_eqn) =>
     error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
diff -r c816b6dcc8af -r 53d6a1c110f1 src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy	Wed Mar 11 19:27:48 2009 +0100
@@ -11,9 +11,9 @@
 lemma contentsI: "y = {x} ==> contents y = x" 
   unfolding contents_def by auto -- {* FIXME move *}
 
-lemmas split_split = prod.split [unfolded prod_case_split] 
+lemmas split_split = prod.split [unfolded prod_case_split]
 lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
-lemmas "split.splits" = split_split split_split_asm 
+lemmas split_splits = split_split split_split_asm
 
 lemmas funpow_0 = funpow.simps(1)
 lemmas funpow_Suc = funpow.simps(2)
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/General/name_space.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -36,7 +36,6 @@
   val root_path: naming -> naming
   val parent_path: naming -> naming
   val no_base_names: naming -> naming
-  val qualified_names: naming -> naming
   val sticky_prefix: string -> naming -> naming
   type 'a table = T * 'a Symtab.table
   val bind: naming -> binding * 'a -> 'a table -> string * 'a table       (*exception Symtab.DUP*)
@@ -174,53 +173,44 @@
 
 datatype naming = Naming of
  {path: (string * bool) list,
-  no_base_names: bool,
-  qualified_names: bool};
+  no_base_names: bool};
 
-fun make_naming (path, no_base_names, qualified_names) =
-  Naming {path = path, no_base_names = no_base_names, qualified_names = qualified_names};
+fun make_naming (path, no_base_names) =
+  Naming {path = path, no_base_names = no_base_names};
 
-fun map_naming f (Naming {path, no_base_names, qualified_names}) =
-  make_naming (f (path, no_base_names, qualified_names));
-
-fun path_of (Naming {path, ...}) = path;
+fun map_naming f (Naming {path, no_base_names}) =
+  make_naming (f (path, no_base_names));
 
 
 (* configure naming *)
 
-val default_naming = make_naming ([], false, false);
+val default_naming = make_naming ([], false);
 
-fun add_path elems = map_naming (fn (path, no_base_names, qualified_names) =>
-  (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
+fun add_path elems = map_naming (fn (path, no_base_names) =>
+  (path @ map (rpair false) (Long_Name.explode elems), no_base_names));
 
-val root_path = map_naming (fn (_, no_base_names, qualified_names) =>
-  ([], no_base_names, qualified_names));
+val root_path = map_naming (fn (_, no_base_names) => ([], no_base_names));
 
-val parent_path = map_naming (fn (path, no_base_names, qualified_names) =>
-  (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names));
+val parent_path = map_naming (fn (path, no_base_names) =>
+  (perhaps (try (#1 o split_last)) path, no_base_names));
 
-fun sticky_prefix elems = map_naming (fn (path, no_base_names, qualified_names) =>
-  (path @ map (rpair true) (Long_Name.explode elems), no_base_names, qualified_names));
+fun sticky_prefix elems = map_naming (fn (path, no_base_names) =>
+  (path @ map (rpair true) (Long_Name.explode elems), no_base_names));
 
-val no_base_names = map_naming (fn (path, _, qualified_names) => (path, true, qualified_names));
-val qualified_names = map_naming (fn (path, no_base_names, _) => (path, no_base_names, true));
+val no_base_names = map_naming (fn (path, _) => (path, true));
 
 
 (* full name *)
 
 fun err_bad binding = error ("Bad name declaration " ^ quote (Binding.str_of binding));
 
-fun name_spec (Naming {path, qualified_names, ...}) binding =
+fun name_spec (Naming {path, ...}) binding =
   let
     val (prefix, name) = Binding.dest binding;
-    val _ = not qualified_names andalso Long_Name.is_qualified name andalso err_bad binding;
+    val _ = Long_Name.is_qualified name andalso err_bad binding;
 
     val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
-    val spec2 =
-      (case try split_last (Long_Name.explode name) of
-        NONE => []
-      | SOME (qual, base) => map (rpair false) qual @ [(base, true)]);
-
+    val spec2 = if name = "" then [] else [(name, true)];
     val spec = spec1 @ spec2;
     val _ =
       exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -42,14 +42,15 @@
           if c <> c' then
             err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
           else ());
+    val b = Binding.name c;
 
     val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
-    val name = Binding.map_name (Thm.def_name_optional c) raw_name;
+    val name = Thm.def_binding_optional b raw_name;
     val atts = map (prep_att thy) raw_atts;
 
     val thy' =
       thy
-      |> Sign.add_consts_i [(Binding.name c, T, mx)]
+      |> Sign.add_consts_i [(b, T, mx)]
       |> PureThy.add_defs false [((name, def), atts)]
       |-> (fn [thm] => Code.add_default_eqn thm);
   in ((c, T), thy') end;
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/element.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -502,7 +502,7 @@
         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
         val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
             let val ((c, _), t') = LocalDefs.cert_def ctxt t
-            in (t', ((Binding.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
+            in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
         val (_, ctxt') =
           ctxt |> fold (Variable.auto_fixes o #1) asms
           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
@@ -518,8 +518,8 @@
     fun activate elem ctxt =
       let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem
       in (elem', activate_elem elem' ctxt) end
-    val (elems, ctxt') = fold_map activate raw_elems (ProofContext.qualified_names ctxt);
-  in (elems |> map (map_ctxt_attrib Args.closure), ProofContext.restore_naming ctxt ctxt') end;
+    val (elems, ctxt') = fold_map activate raw_elems ctxt;
+  in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end;
 
 fun check_name name =
   if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name)
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -304,7 +304,7 @@
             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
         | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
             let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
-            in ((Binding.map_name (Thm.def_name_optional c) name, atts), (t', no_binds ps)) end))
+            in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
         | e => e)
       end;
 
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -91,7 +91,7 @@
     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 names = map2 (Binding.map_name o Thm.def_name_optional) xs bfacts;
+    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;
   in
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -138,14 +138,12 @@
 
 fun full_naming lthy =
   Sign.naming_of (ProofContext.theory_of lthy)
-  |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
-  |> NameSpace.qualified_names;
+  |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy));
 
 fun full_name naming = NameSpace.full_name (full_naming naming);
 
 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
   |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
-  |> Sign.qualified_names
   |> f
   ||> Sign.restore_naming thy);
 
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -107,19 +107,6 @@
 
 datatype ctxt = datatype Element.ctxt;
 
-fun global_note_qualified kind facts thy = (*FIXME*)
-  thy
-  |> Sign.qualified_names
-  |> PureThy.note_thmss kind facts
-  ||> Sign.restore_naming thy;
-
-fun local_note_qualified kind facts ctxt = (*FIXME*)
-  ctxt
-  |> ProofContext.qualified_names
-  |> ProofContext.note_thmss_i kind facts
-  ||> ProofContext.restore_naming ctxt;
-
-
 
 (*** Theory data ***)
 
@@ -337,7 +324,7 @@
 fun init_global_elem (Notes (kind, facts)) thy =
   let
     val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
-  in global_note_qualified kind facts' thy |> snd end
+  in PureThy.note_thmss kind facts' thy |> snd end
 
 fun init_local_elem (Fixes fixes) ctxt = ctxt |>
       ProofContext.add_fixes_i fixes |> snd
@@ -359,7 +346,7 @@
   | init_local_elem (Notes (kind, facts)) ctxt =
       let
         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
-      in local_note_qualified kind facts' ctxt |> snd end
+      in ProofContext.note_thmss_i kind facts' ctxt |> snd end
 
 fun cons_elem false (Notes notes) elems = elems
   | cons_elem _ elem elems = elem :: elems
@@ -452,7 +439,7 @@
             let
               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
                 Attrib.map_facts (Attrib.attribute_i thy)
-            in global_note_qualified kind args'' #> snd end)
+            in PureThy.note_thmss kind args'' #> snd end)
         (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
   in ctxt'' end;
 
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -98,7 +98,6 @@
   val get_thm: Proof.context -> xstring -> thm
   val add_path: string -> Proof.context -> Proof.context
   val sticky_prefix: string -> Proof.context -> Proof.context
-  val qualified_names: Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val reset_naming: Proof.context -> Proof.context
   val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
@@ -947,7 +946,6 @@
 
 val add_path        = map_naming o NameSpace.add_path;
 val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
-val qualified_names = map_naming NameSpace.qualified_names;
 val restore_naming  = map_naming o K o naming_of;
 val reset_naming    = map_naming (K local_naming);
 
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -169,8 +169,7 @@
     val (vars, [((raw_name, atts), [prop])]) =
       fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
     val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
-    val name = Binding.map_name (Thm.def_name_optional x) raw_name;
-    val var =
+    val var as (b, _) =
       (case vars of
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
@@ -180,9 +179,12 @@
               error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
           in (b, mx) end);
-    val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
+    val name = Thm.def_binding_optional b raw_name;
+    val ((lhs, (_, th)), lthy2) = lthy
+      |> LocalTheory.define Thm.definitionK
         (var, ((Binding.suffix_name "_raw" name, []), rhs));
-    val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
+    val ((def_name, [th']), lthy3) = lthy2
+      |> LocalTheory.note Thm.definitionK
         ((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
 
     val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -1,5 +1,6 @@
 (*  Title:      Pure/Isar/theory_target.ML
     Author:     Makarius
+    Author:     Florian Haftmann, TU Muenchen
 
 Common theory/locale/class/instantiation/overloading targets.
 *)
@@ -48,10 +49,10 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
-    val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
-      (#1 (ProofContext.inferred_fixes ctxt));
-    val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
-      (Assumption.assms_of ctxt);
+    val fixes =
+      map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
+    val assumes =
+      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.assms_of ctxt);
     val elems =
       (if null fixes then [] else [Element.Fixes fixes]) @
       (if null assumes then [] else [Element.Assumes assumes]);
@@ -143,12 +144,6 @@
 
   in (result'', result) end;
 
-fun note_local kind facts ctxt =
-  ctxt
-  |> ProofContext.qualified_names
-  |> ProofContext.note_thmss_i kind facts
-  ||> ProofContext.restore_naming ctxt;
-
 fun notes (Target {target, is_locale, ...}) kind facts lthy =
   let
     val thy = ProofContext.theory_of lthy;
@@ -164,12 +159,10 @@
       |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy);
   in
     lthy |> LocalTheory.theory
-      (Sign.qualified_names
-        #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
-        #> Sign.restore_naming thy)
-    |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
+      (PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
+    |> not is_locale ? LocalTheory.target (ProofContext.note_thmss_i kind global_facts #> snd)
     |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
-    |> note_local kind local_facts
+    |> ProofContext.note_thmss_i kind local_facts
   end;
 
 
@@ -195,8 +188,8 @@
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
-        (fn thy => thy |> 
-          Sign.no_base_names
+        (fn thy => thy
+          |> Sign.no_base_names
           |> Sign.add_abbrev PrintMode.internal tags legacy_arg
           ||> Sign.restore_naming thy)
         (ProofContext.add_abbrev PrintMode.internal tags arg)
@@ -210,7 +203,7 @@
 
 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   let
-    val c = Binding.name_of b;  (* FIXME Binding.qualified_name_of *)
+    val c = Binding.qualified_name_of b;
     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;
@@ -278,8 +271,7 @@
     val thy = ProofContext.theory_of lthy;
     val thy_ctxt = ProofContext.init thy;
 
-    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 name' = Thm.def_binding_optional 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' [];
@@ -290,6 +282,7 @@
     val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
 
     (*def*)
+    val c = Binding.qualified_name_of b;
     val define_const =
       (case Overloading.operation lthy c of
         SOME (_, checked) =>
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -732,12 +732,12 @@
              val fu = Type.freeze u;
              val (def_thms, thy') = if t = nullt then ([], thy) else
                thy
-               |> 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"),
+               |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
+               |> PureThy.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"),
                     Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
            in
              thy'
-             |> PureThy.store_thm (Binding.name (corr_name s vs),
+             |> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
                   Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop))
                     (Thm.forall_elim_var 0) (forall_intr_frees
                       (ProofChecker.thm_of_proof thy'
@@ -749,7 +749,7 @@
 
   in
     thy
-    |> Sign.absolute_path
+    |> Sign.root_path
     |> fold_rev add_def defs
     |> Sign.restore_naming thy
   end;
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -36,8 +36,8 @@
 
 fun add_proof_atom_consts names thy =
   thy
-  |> Sign.absolute_path
-  |> Sign.add_consts_i (map (fn name => (Binding.name name, proofT, NoSyn)) names);
+  |> Sign.root_path
+  |> Sign.add_consts_i (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
 
 (** constants for application and abstraction **)
 
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/more_thm.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -57,6 +57,7 @@
   val default_position_of: thm -> thm -> thm
   val def_name: string -> string
   val def_name_optional: string -> string -> string
+  val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
   val put_name_hint: string -> thm -> thm
@@ -353,6 +354,9 @@
 fun def_name_optional c "" = def_name c
   | def_name_optional _ name = name;
 
+fun def_binding_optional b name =
+  if Binding.is_empty name then Binding.map_name def_name b else name;
+
 
 (* unofficial theorem names *)
 
diff -r c816b6dcc8af -r 53d6a1c110f1 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/sign.ML	Wed Mar 11 19:27:48 2009 +0100
@@ -126,8 +126,6 @@
   val parent_path: theory -> theory
   val sticky_prefix: string -> theory -> theory
   val no_base_names: theory -> theory
-  val qualified_names: theory -> theory
-  val absolute_path: theory -> theory
   val local_path: theory -> theory
   val restore_naming: theory -> theory -> theory
   val hide_class: bool -> string -> theory -> theory
@@ -623,9 +621,6 @@
 val parent_path     = map_naming NameSpace.parent_path;
 val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val no_base_names   = map_naming NameSpace.no_base_names;
-val qualified_names = map_naming NameSpace.qualified_names;
-
-val absolute_path = root_path o qualified_names;
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);