Name.qualified;
authorwenzelm
Wed Sep 03 11:44:48 2008 +0200 (2008-09-03)
changeset 28107760ecc6fc1bd
parent 28106 48b9c8756020
child 28108 1b08ed83b79e
Name.qualified;
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Sep 03 11:27:15 2008 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Sep 03 11:44:48 2008 +0200
     1.3 @@ -673,7 +673,7 @@
     1.4        elims raw_induct ctxt =
     1.5    let
     1.6      val rec_name = Name.name_of rec_binding;
     1.7 -    val rec_qualified = NameSpace.qualified rec_name;
     1.8 +    val rec_qualified = Name.qualified rec_name;
     1.9      val intr_names = map Name.name_of intr_bindings;
    1.10      val ind_case_names = RuleCases.case_names intr_names;
    1.11      val induct =
    1.12 @@ -688,13 +688,12 @@
    1.13      val (intrs', ctxt1) =
    1.14        ctxt |>
    1.15        LocalTheory.notes kind
    1.16 -        (map (Name.map_name rec_qualified) intr_bindings ~~
    1.17 -         intr_atts ~~ map (fn th => [([th],
    1.18 +        (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
    1.19             [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
    1.20        map (hd o snd);
    1.21      val (((_, elims'), (_, [induct'])), ctxt2) =
    1.22        ctxt1 |>
    1.23 -      LocalTheory.note kind ((Name.binding (rec_qualified "intros"), []), intrs') ||>>
    1.24 +      LocalTheory.note kind ((rec_qualified (Name.binding "intros"), []), intrs') ||>>
    1.25        fold_map (fn (name, (elim, cases)) =>
    1.26          LocalTheory.note kind ((Name.binding (NameSpace.qualified (Sign.base_name name) "cases"),
    1.27            [Attrib.internal (K (RuleCases.case_names cases)),
    1.28 @@ -702,14 +701,15 @@
    1.29             Attrib.internal (K (Induct.cases_pred name)),
    1.30             Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
    1.31          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
    1.32 -      LocalTheory.note kind ((Name.binding (rec_qualified (coind_prefix coind ^ "induct")),
    1.33 -        map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
    1.34 +      LocalTheory.note kind
    1.35 +        ((rec_qualified (Name.binding (coind_prefix coind ^ "induct")),
    1.36 +          map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
    1.37  
    1.38      val ctxt3 = if no_ind orelse coind then ctxt2 else
    1.39        let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
    1.40        in
    1.41          ctxt2 |>
    1.42 -        LocalTheory.notes kind [((Name.binding (rec_qualified "inducts"), []),
    1.43 +        LocalTheory.notes kind [((rec_qualified (Name.binding "inducts"), []),
    1.44            inducts |> map (fn (name, th) => ([th],
    1.45              [Attrib.internal (K ind_case_names),
    1.46               Attrib.internal (K (RuleCases.consumes 1)),
     2.1 --- a/src/HOL/Tools/primrec_package.ML	Wed Sep 03 11:27:15 2008 +0200
     2.2 +++ b/src/HOL/Tools/primrec_package.ML	Wed Sep 03 11:44:48 2008 +0200
     2.3 @@ -248,9 +248,9 @@
     2.4      val _ = if gen_eq_set (op =) (names1, names2) then ()
     2.5        else primrec_error ("functions " ^ commas_quote names2 ^
     2.6          "\nare not mutually recursive");
     2.7 -    val qualify = NameSpace.qualified
     2.8 +    val qualify = Name.qualified
     2.9        (space_implode "_" (map (Sign.base_name o #1) defs));
    2.10 -    val spec' = (map o apfst o apfst o Name.map_name) qualify spec;
    2.11 +    val spec' = (map o apfst o apfst) qualify spec;
    2.12      val simp_atts = map (Attrib.internal o K)
    2.13        [Simplifier.simp_add, RecfunCodegen.add NONE];
    2.14    in
    2.15 @@ -260,7 +260,7 @@
    2.16      |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
    2.17      |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
    2.18      |-> (fn simps' => LocalTheory.note Thm.theoremK
    2.19 -          ((Name.binding (qualify "simps"), simp_atts), maps snd simps'))
    2.20 +          ((qualify (Name.binding "simps"), simp_atts), maps snd simps'))
    2.21      |>> snd
    2.22    end handle PrimrecError (msg, some_eqn) =>
    2.23      error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
     3.1 --- a/src/Pure/Isar/locale.ML	Wed Sep 03 11:27:15 2008 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Wed Sep 03 11:44:48 2008 +0200
     3.3 @@ -1560,8 +1560,7 @@
     3.4  
     3.5  (* naming of interpreted theorems *)
     3.6  
     3.7 -fun add_param_prefixss s =
     3.8 -  (map o apfst o apfst o Name.map_name) (NameSpace.qualified s);
     3.9 +fun add_param_prefixss s = (map o apfst o apfst) (Name.qualified s);
    3.10  fun drop_param_prefixss args = (map o apfst o apfst o Name.map_name)
    3.11    (fn "" => "" | s => (NameSpace.implode o tl o NameSpace.explode) s) args;
    3.12  
    3.13 @@ -1649,7 +1648,7 @@
    3.14  
    3.15  fun interpret_args thy prfx insts prems eqns exp attrib args =
    3.16    let
    3.17 -    val inst = Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
    3.18 +    val inst = Morphism.name_morphism (Name.qualified prfx) $>
    3.19  (* need to add parameter prefix *) (* FIXME *)
    3.20        Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
    3.21        Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
    3.22 @@ -2361,7 +2360,7 @@
    3.23              fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
    3.24                  let
    3.25                    val att_morphism =
    3.26 -                    Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
    3.27 +                    Morphism.name_morphism (Name.qualified prfx) $>
    3.28                      Morphism.thm_morphism satisfy $>
    3.29                      Element.inst_morphism thy insts $>
    3.30                      Morphism.thm_morphism disch;