src/HOL/Nominal/nominal_inductive.ML
changeset 33671 4b0f2599ed48
parent 33670 02b7738aef6a
child 33772 b6a1feca2ac2
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 13 20:41:29 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 13 21:11:15 2009 +0100
     1.3 @@ -561,19 +561,19 @@
     1.4              (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
     1.5            else (strong_raw_induct RSN (2, rev_mp),
     1.6              [ind_case_names, Rule_Cases.consumes 1]);
     1.7 -        val ((_, [strong_induct']), ctxt') = ctxt |> LocalTheory.note
     1.8 +        val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
     1.9            ((rec_qualified (Binding.name "strong_induct"),
    1.10              map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
    1.11          val strong_inducts =
    1.12            Project_Rule.projects ctxt (1 upto length names) strong_induct';
    1.13        in
    1.14          ctxt' |>
    1.15 -        LocalTheory.note
    1.16 +        Local_Theory.note
    1.17            ((rec_qualified (Binding.name "strong_inducts"),
    1.18              [Attrib.internal (K ind_case_names),
    1.19               Attrib.internal (K (Rule_Cases.consumes 1))]),
    1.20             strong_inducts) |> snd |>
    1.21 -        LocalTheory.notes (map (fn ((name, elim), (_, cases)) =>
    1.22 +        Local_Theory.notes (map (fn ((name, elim), (_, cases)) =>
    1.23              ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
    1.24                [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
    1.25                 Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
    1.26 @@ -663,7 +663,7 @@
    1.27        end) atoms
    1.28    in
    1.29      ctxt |>
    1.30 -    LocalTheory.notes (map (fn (name, ths) =>
    1.31 +    Local_Theory.notes (map (fn (name, ths) =>
    1.32          ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
    1.33            [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
    1.34        (names ~~ transp thss)) |> snd