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