# HG changeset patch
# User wenzelm
# Date 1220435088 -7200
# Node ID 760ecc6fc1bd93cb7ba9065222a0dd3649761b21
# Parent  48b9c8756020d6839afa720fe59bc9eff111af8e
Name.qualified;

diff -r 48b9c8756020 -r 760ecc6fc1bd src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Sep 03 11:27:15 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Sep 03 11:44:48 2008 +0200
@@ -673,7 +673,7 @@
       elims raw_induct ctxt =
   let
     val rec_name = Name.name_of rec_binding;
-    val rec_qualified = NameSpace.qualified rec_name;
+    val rec_qualified = Name.qualified rec_name;
     val intr_names = map Name.name_of intr_bindings;
     val ind_case_names = RuleCases.case_names intr_names;
     val induct =
@@ -688,13 +688,12 @@
     val (intrs', ctxt1) =
       ctxt |>
       LocalTheory.notes kind
-        (map (Name.map_name rec_qualified) intr_bindings ~~
-         intr_atts ~~ map (fn th => [([th],
+        (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
            [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), ctxt2) =
       ctxt1 |>
-      LocalTheory.note kind ((Name.binding (rec_qualified "intros"), []), intrs') ||>>
+      LocalTheory.note kind ((rec_qualified (Name.binding "intros"), []), intrs') ||>>
       fold_map (fn (name, (elim, cases)) =>
         LocalTheory.note kind ((Name.binding (NameSpace.qualified (Sign.base_name name) "cases"),
           [Attrib.internal (K (RuleCases.case_names cases)),
@@ -702,14 +701,15 @@
            Attrib.internal (K (Induct.cases_pred name)),
            Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
         apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
-      LocalTheory.note kind ((Name.binding (rec_qualified (coind_prefix coind ^ "induct")),
-        map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
+      LocalTheory.note kind
+        ((rec_qualified (Name.binding (coind_prefix coind ^ "induct")),
+          map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
 
     val ctxt3 = if no_ind orelse coind then ctxt2 else
       let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
       in
         ctxt2 |>
-        LocalTheory.notes kind [((Name.binding (rec_qualified "inducts"), []),
+        LocalTheory.notes kind [((rec_qualified (Name.binding "inducts"), []),
           inducts |> map (fn (name, th) => ([th],
             [Attrib.internal (K ind_case_names),
              Attrib.internal (K (RuleCases.consumes 1)),
diff -r 48b9c8756020 -r 760ecc6fc1bd src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed Sep 03 11:27:15 2008 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Wed Sep 03 11:44:48 2008 +0200
@@ -248,9 +248,9 @@
     val _ = if gen_eq_set (op =) (names1, names2) then ()
       else primrec_error ("functions " ^ commas_quote names2 ^
         "\nare not mutually recursive");
-    val qualify = NameSpace.qualified
+    val qualify = Name.qualified
       (space_implode "_" (map (Sign.base_name o #1) defs));
-    val spec' = (map o apfst o apfst o Name.map_name) qualify spec;
+    val spec' = (map o apfst o apfst) qualify spec;
     val simp_atts = map (Attrib.internal o K)
       [Simplifier.simp_add, RecfunCodegen.add NONE];
   in
@@ -260,7 +260,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
-          ((Name.binding (qualify "simps"), simp_atts), maps snd simps'))
+          ((qualify (Name.binding "simps"), simp_atts), maps snd simps'))
     |>> snd
   end handle PrimrecError (msg, some_eqn) =>
     error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
diff -r 48b9c8756020 -r 760ecc6fc1bd src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Sep 03 11:27:15 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Sep 03 11:44:48 2008 +0200
@@ -1560,8 +1560,7 @@
 
 (* naming of interpreted theorems *)
 
-fun add_param_prefixss s =
-  (map o apfst o apfst o Name.map_name) (NameSpace.qualified s);
+fun add_param_prefixss s = (map o apfst o apfst) (Name.qualified s);
 fun drop_param_prefixss args = (map o apfst o apfst o Name.map_name)
   (fn "" => "" | s => (NameSpace.implode o tl o NameSpace.explode) s) args;
 
@@ -1649,7 +1648,7 @@
 
 fun interpret_args thy prfx insts prems eqns exp attrib args =
   let
-    val inst = Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
+    val inst = Morphism.name_morphism (Name.qualified prfx) $>
 (* need to add parameter prefix *) (* FIXME *)
       Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
       Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
@@ -2361,7 +2360,7 @@
             fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
                 let
                   val att_morphism =
-                    Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
+                    Morphism.name_morphism (Name.qualified prfx) $>
                     Morphism.thm_morphism satisfy $>
                     Element.inst_morphism thy insts $>
                     Morphism.thm_morphism disch;