mandatory prefix where appropriate
authorhaftmann
Wed Sep 30 08:22:07 2009 +0200 (2009-09-30)
changeset 32773f6fd4ccd8eea
parent 32772 50d090ca93f8
child 32774 461afcc6acb8
mandatory prefix where appropriate
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Wed Sep 30 08:21:53 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Wed Sep 30 08:22:07 2009 +0200
     1.3 @@ -683,7 +683,7 @@
     1.4        elims raw_induct ctxt =
     1.5    let
     1.6      val rec_name = Binding.name_of rec_binding;
     1.7 -    val rec_qualified = Binding.qualify false rec_name;
     1.8 +    fun rec_qualified qualified = Binding.qualify qualified rec_name;
     1.9      val intr_names = map Binding.name_of intr_bindings;
    1.10      val ind_case_names = RuleCases.case_names intr_names;
    1.11      val induct =
    1.12 @@ -698,29 +698,29 @@
    1.13      val (intrs', ctxt1) =
    1.14        ctxt |>
    1.15        LocalTheory.notes kind
    1.16 -        (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
    1.17 +        (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
    1.18             [Attrib.internal (K (ContextRules.intro_query NONE)),
    1.19              Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>>
    1.20        map (hd o snd);
    1.21      val (((_, elims'), (_, [induct'])), ctxt2) =
    1.22        ctxt1 |>
    1.23 -      LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>>
    1.24 +      LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
    1.25        fold_map (fn (name, (elim, cases)) =>
    1.26 -        LocalTheory.note kind ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "cases"),
    1.27 +        LocalTheory.note kind ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
    1.28            [Attrib.internal (K (RuleCases.case_names cases)),
    1.29             Attrib.internal (K (RuleCases.consumes 1)),
    1.30             Attrib.internal (K (Induct.cases_pred name)),
    1.31             Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
    1.32          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
    1.33        LocalTheory.note kind
    1.34 -        ((rec_qualified (Binding.name (coind_prefix coind ^ "induct")),
    1.35 +        ((rec_qualified true (Binding.name (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 ~~ Project_Rule.projects ctxt2 (1 upto length cnames) induct'
    1.40        in
    1.41          ctxt2 |>
    1.42 -        LocalTheory.notes kind [((rec_qualified (Binding.name "inducts"), []),
    1.43 +        LocalTheory.notes kind [((rec_qualified true (Binding.name "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)),