eliminated slightly odd kind argument of LocalTheory.note(s);
authorwenzelm
Fri Nov 13 20:41:29 2009 +0100 (2009-11-13)
changeset 3367002b7738aef6a
parent 33669 ae9a2ea9a989
child 33671 4b0f2599ed48
eliminated slightly odd kind argument of LocalTheory.note(s);
added LocalTheory.notes_kind as fall-back for unusual cases;
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOLCF/Tools/fixrec.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
     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
     2.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 13 19:57:46 2009 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 13 20:41:29 2009 +0100
     2.3 @@ -466,15 +466,14 @@
     2.4              NONE => (rec_qualified (Binding.name "strong_induct"),
     2.5                       rec_qualified (Binding.name "strong_inducts"))
     2.6            | SOME s => (Binding.name s, Binding.name (s ^ "s"));
     2.7 -        val ((_, [strong_induct']), ctxt') = LocalTheory.note ""
     2.8 +        val ((_, [strong_induct']), ctxt') = ctxt |> LocalTheory.note
     2.9            ((induct_name,
    2.10 -            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
    2.11 -          ctxt;
    2.12 +            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
    2.13          val strong_inducts =
    2.14            Project_Rule.projects ctxt' (1 upto length names) strong_induct'
    2.15        in
    2.16          ctxt' |>
    2.17 -        LocalTheory.note ""
    2.18 +        LocalTheory.note
    2.19            ((inducts_name,
    2.20              [Attrib.internal (K ind_case_names),
    2.21               Attrib.internal (K (Rule_Cases.consumes 1))]),
     3.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 19:57:46 2009 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 20:41:29 2009 +0100
     3.3 @@ -367,11 +367,10 @@
     3.4        (fn thss => fn goal_ctxt =>
     3.5           let
     3.6             val simps = ProofContext.export goal_ctxt lthy' (flat thss);
     3.7 -           val (simps', lthy'') = fold_map (LocalTheory.note "")
     3.8 -             (names_atts' ~~ map single simps) lthy'
     3.9 +           val (simps', lthy'') = fold_map LocalTheory.note (names_atts' ~~ map single simps) lthy';
    3.10           in
    3.11             lthy''
    3.12 -           |> LocalTheory.note "" ((qualify (Binding.name "simps"),
    3.13 +           |> LocalTheory.note ((qualify (Binding.name "simps"),
    3.14                  map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
    3.15                  maps snd simps')
    3.16             |> snd
     4.1 --- a/src/HOL/Tools/Function/function.ML	Fri Nov 13 19:57:46 2009 +0100
     4.2 +++ b/src/HOL/Tools/Function/function.ML	Fri Nov 13 20:41:29 2009 +0100
     4.3 @@ -43,9 +43,6 @@
     4.4      [Simplifier.simp_add,
     4.5       Nitpick_Psimps.add]
     4.6  
     4.7 -fun note_theorem ((binding, atts), ths) =
     4.8 -  LocalTheory.note "" ((binding, atts), ths)
     4.9 -
    4.10  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
    4.11  
    4.12  fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy =
    4.13 @@ -55,13 +52,13 @@
    4.14                     |> map (apfst (apfst extra_qualify))
    4.15  
    4.16        val (saved_spec_simps, lthy) =
    4.17 -        fold_map (LocalTheory.note "") spec lthy
    4.18 +        fold_map LocalTheory.note spec lthy
    4.19  
    4.20        val saved_simps = maps snd saved_spec_simps
    4.21        val simps_by_f = sort saved_simps
    4.22  
    4.23        fun add_for_f fname simps =
    4.24 -        note_theorem ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
    4.25 +        LocalTheory.note ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
    4.26          #> snd
    4.27      in
    4.28        (saved_simps,
    4.29 @@ -100,14 +97,14 @@
    4.30              |> addsmps (conceal_partial o Binding.qualify false "partial")
    4.31                   "psimps" conceal_partial psimp_attribs psimps
    4.32              ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
    4.33 -            ||>> note_theorem ((conceal_partial (qualify "pinduct"),
    4.34 +            ||>> LocalTheory.note ((conceal_partial (qualify "pinduct"),
    4.35                     [Attrib.internal (K (Rule_Cases.case_names cnames)),
    4.36                      Attrib.internal (K (Rule_Cases.consumes 1)),
    4.37                      Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
    4.38 -            ||>> note_theorem ((Binding.conceal (qualify "termination"), []), [termination])
    4.39 -            ||> (snd o note_theorem ((qualify "cases",
    4.40 +            ||>> LocalTheory.note ((Binding.conceal (qualify "termination"), []), [termination])
    4.41 +            ||> (snd o LocalTheory.note ((qualify "cases",
    4.42                     [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
    4.43 -            ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
    4.44 +            ||> fold_option (snd oo curry LocalTheory.note (qualify "domintros", [])) domintros
    4.45  
    4.46            val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
    4.47                                        pinducts=snd pinducts', termination=termination',
    4.48 @@ -155,7 +152,7 @@
    4.49            in
    4.50              lthy
    4.51              |> add_simps I "simps" I simp_attribs tsimps |> snd
    4.52 -            |> note_theorem
    4.53 +            |> LocalTheory.note
    4.54                 ((qualify "induct",
    4.55                   [Attrib.internal (K (Rule_Cases.case_names case_names))]),
    4.56                  tinduct) |> snd
     5.1 --- a/src/HOL/Tools/inductive.ML	Fri Nov 13 19:57:46 2009 +0100
     5.2 +++ b/src/HOL/Tools/inductive.ML	Fri Nov 13 20:41:29 2009 +0100
     5.3 @@ -469,7 +469,7 @@
     5.4      val facts = args |> map (fn ((a, atts), props) =>
     5.5        ((a, map (prep_att thy) atts),
     5.6          map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
     5.7 -  in lthy |> LocalTheory.notes "" facts |>> map snd end;
     5.8 +  in lthy |> LocalTheory.notes facts |>> map snd end;
     5.9  
    5.10  val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
    5.11  val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
    5.12 @@ -695,7 +695,7 @@
    5.13  
    5.14      val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'';
    5.15      val ((_, [mono']), lthy''') =
    5.16 -      LocalTheory.note "" (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
    5.17 +      LocalTheory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
    5.18  
    5.19    in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
    5.20      list_comb (rec_const, params), preds, argTs, bs, xs)
    5.21 @@ -719,7 +719,7 @@
    5.22  
    5.23      val (intrs', lthy1) =
    5.24        lthy |>
    5.25 -      LocalTheory.notes ""
    5.26 +      LocalTheory.notes
    5.27          (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
    5.28            map (fn th => [([th],
    5.29             [Attrib.internal (K (Context_Rules.intro_query NONE)),
    5.30 @@ -727,16 +727,16 @@
    5.31        map (hd o snd);
    5.32      val (((_, elims'), (_, [induct'])), lthy2) =
    5.33        lthy1 |>
    5.34 -      LocalTheory.note "" ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
    5.35 +      LocalTheory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
    5.36        fold_map (fn (name, (elim, cases)) =>
    5.37 -        LocalTheory.note ""
    5.38 +        LocalTheory.note
    5.39            ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
    5.40              [Attrib.internal (K (Rule_Cases.case_names cases)),
    5.41               Attrib.internal (K (Rule_Cases.consumes 1)),
    5.42               Attrib.internal (K (Induct.cases_pred name)),
    5.43               Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
    5.44          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
    5.45 -      LocalTheory.note ""
    5.46 +      LocalTheory.note
    5.47          ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
    5.48            map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
    5.49  
    5.50 @@ -745,7 +745,7 @@
    5.51        else
    5.52          let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in
    5.53            lthy2 |>
    5.54 -          LocalTheory.notes "" [((rec_qualified true (Binding.name "inducts"), []),
    5.55 +          LocalTheory.notes [((rec_qualified true (Binding.name "inducts"), []),
    5.56              inducts |> map (fn (name, th) => ([th],
    5.57                [Attrib.internal (K ind_case_names),
    5.58                 Attrib.internal (K (Rule_Cases.consumes 1)),
     6.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Nov 13 19:57:46 2009 +0100
     6.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Nov 13 20:41:29 2009 +0100
     6.3 @@ -505,7 +505,7 @@
     6.4              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
     6.5                [def, mem_Collect_eq, split_conv]) 1))
     6.6          in
     6.7 -          lthy |> LocalTheory.note "" ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
     6.8 +          lthy |> LocalTheory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
     6.9              [Attrib.internal (K pred_set_conv_att)]),
    6.10                [conv_thm]) |> snd
    6.11          end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;
     7.1 --- a/src/HOL/Tools/primrec.ML	Fri Nov 13 19:57:46 2009 +0100
     7.2 +++ b/src/HOL/Tools/primrec.ML	Fri Nov 13 20:41:29 2009 +0100
     7.3 @@ -277,8 +277,8 @@
     7.4      lthy
     7.5      |> set_group ? LocalTheory.set_group (serial ())
     7.6      |> add_primrec_simple fixes (map snd spec)
     7.7 -    |-> (fn (prefix, simps) => fold_map (LocalTheory.note "") (attr_bindings prefix ~~ simps)
     7.8 -      #-> (fn simps' => LocalTheory.note "" (simp_attr_binding prefix, maps snd simps')))
     7.9 +    |-> (fn (prefix, simps) => fold_map LocalTheory.note (attr_bindings prefix ~~ simps)
    7.10 +      #-> (fn simps' => LocalTheory.note (simp_attr_binding prefix, maps snd simps')))
    7.11      |>> snd
    7.12    end;
    7.13  
     8.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 19:57:46 2009 +0100
     8.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 20:41:29 2009 +0100
     8.3 @@ -214,7 +214,7 @@
     8.4      lthy
     8.5      |> random_aux_primrec_multi (name ^ prfx) proto_eqs
     8.6      |-> (fn proto_simps => prove_simps proto_simps)
     8.7 -    |-> (fn simps => LocalTheory.note ""
     8.8 +    |-> (fn simps => LocalTheory.note
     8.9        ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    8.10            [Simplifier.simp_add, Nitpick_Simps.add]), simps))
    8.11      |> snd
     9.1 --- a/src/HOLCF/Tools/fixrec.ML	Fri Nov 13 19:57:46 2009 +0100
     9.2 +++ b/src/HOLCF/Tools/fixrec.ML	Fri Nov 13 20:41:29 2009 +0100
     9.3 @@ -242,7 +242,7 @@
     9.4          ((thm_name, [src]), [thm])
     9.5        end;
     9.6      val (thmss, lthy'') = lthy'
     9.7 -      |> fold_map (LocalTheory.note "") (induct_note :: map unfold_note unfold_thms);
     9.8 +      |> fold_map LocalTheory.note (induct_note :: map unfold_note unfold_thms);
     9.9    in
    9.10      (lthy'', names, fixdef_thms, map snd unfold_thms)
    9.11    end;
    9.12 @@ -464,7 +464,7 @@
    9.13        val simps2 : (Attrib.binding * thm list) list =
    9.14          map (apsnd (fn thm => [thm])) (flat simps);
    9.15        val (_, lthy'') = lthy'
    9.16 -        |> fold_map (LocalTheory.note "") (simps1 @ simps2);
    9.17 +        |> fold_map LocalTheory.note (simps1 @ simps2);
    9.18      in
    9.19        lthy''
    9.20      end
    10.1 --- a/src/Pure/Isar/expression.ML	Fri Nov 13 19:57:46 2009 +0100
    10.2 +++ b/src/Pure/Isar/expression.ML	Fri Nov 13 20:41:29 2009 +0100
    10.3 @@ -775,7 +775,7 @@
    10.4        |> Locale.register_locale binding (extraTs, params)
    10.5            (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
    10.6        |> Theory_Target.init (SOME name)
    10.7 -      |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
    10.8 +      |> fold (fn (kind, facts) => LocalTheory.notes_kind kind facts #> snd) notes';
    10.9  
   10.10    in (name, loc_ctxt) end;
   10.11  
    11.1 --- a/src/Pure/Isar/local_theory.ML	Fri Nov 13 19:57:46 2009 +0100
    11.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Nov 13 20:41:29 2009 +0100
    11.3 @@ -33,8 +33,10 @@
    11.4      (term * term) * local_theory
    11.5    val define: string -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    11.6      (term * (string * thm)) * local_theory
    11.7 -  val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
    11.8 -  val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    11.9 +  val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
   11.10 +  val notes: (Attrib.binding * (thm list * Attrib.src list) list) list ->
   11.11 +    local_theory -> (string * thm list) list * local_theory
   11.12 +  val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
   11.13      local_theory -> (string * thm list) list * local_theory
   11.14    val type_syntax: bool -> declaration -> local_theory -> local_theory
   11.15    val term_syntax: bool -> declaration -> local_theory -> local_theory
   11.16 @@ -186,12 +188,13 @@
   11.17  val pretty = operation #pretty;
   11.18  val abbrev = apsnd checkpoint ooo operation2 #abbrev;
   11.19  val define = apsnd checkpoint ooo operation2 #define;
   11.20 -val notes = apsnd checkpoint ooo operation2 #notes;
   11.21 +val notes_kind = apsnd checkpoint ooo operation2 #notes;
   11.22  val type_syntax = checkpoint ooo operation2 #type_syntax;
   11.23  val term_syntax = checkpoint ooo operation2 #term_syntax;
   11.24  val declaration = checkpoint ooo operation2 #declaration;
   11.25  
   11.26 -fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
   11.27 +val notes = notes_kind "";
   11.28 +fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
   11.29  
   11.30  fun notation add mode raw_args lthy =
   11.31    let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
    12.1 --- a/src/Pure/Isar/specification.ML	Fri Nov 13 19:57:46 2009 +0100
    12.2 +++ b/src/Pure/Isar/specification.ML	Fri Nov 13 20:41:29 2009 +0100
    12.3 @@ -208,10 +208,10 @@
    12.4      val th = prove lthy2 raw_th;
    12.5      val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
    12.6  
    12.7 -    val ((def_name, [th']), lthy4) = lthy3
    12.8 -      |> LocalTheory.note Thm.definitionK
    12.9 -        ((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
   12.10 -            Code.add_default_eqn_attrib :: atts), [th]);
   12.11 +    val ([(def_name, [th'])], lthy4) = lthy3
   12.12 +      |> LocalTheory.notes_kind Thm.definitionK
   12.13 +        [((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
   12.14 +            Code.add_default_eqn_attrib :: atts), [([th], [])])];
   12.15  
   12.16      val lhs' = Morphism.term (LocalTheory.target_morphism lthy4) lhs;
   12.17      val _ =
   12.18 @@ -270,7 +270,7 @@
   12.19      val facts = raw_facts |> map (fn ((name, atts), bs) =>
   12.20        ((name, map attrib atts),
   12.21          bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
   12.22 -    val (res, lthy') = lthy |> LocalTheory.notes kind facts;
   12.23 +    val (res, lthy') = lthy |> LocalTheory.notes_kind kind facts;
   12.24      val _ = Proof_Display.print_results true lthy' ((kind, ""), res);
   12.25    in (res, lthy') end;
   12.26  
   12.27 @@ -359,14 +359,15 @@
   12.28          burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results
   12.29        in
   12.30          lthy
   12.31 -        |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
   12.32 +        |> LocalTheory.notes_kind kind
   12.33 +          (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
   12.34          |> (fn (res, lthy') =>
   12.35            if Binding.is_empty name andalso null atts then
   12.36              (Proof_Display.print_results true lthy' ((kind, ""), res); lthy')
   12.37            else
   12.38              let
   12.39                val ([(res_name, _)], lthy'') = lthy'
   12.40 -                |> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
   12.41 +                |> LocalTheory.notes_kind kind [((name, atts), [(maps #2 res, [])])];
   12.42                val _ = Proof_Display.print_results true lthy' ((kind, res_name), res);
   12.43              in lthy'' end)
   12.44          |> after_qed results'
    13.1 --- a/src/Pure/Isar/theory_target.ML	Fri Nov 13 19:57:46 2009 +0100
    13.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Nov 13 20:41:29 2009 +0100
    13.3 @@ -310,7 +310,8 @@
    13.4  local
    13.5  
    13.6  fun init_target _ NONE = global_target
    13.7 -  | init_target thy (SOME target) = if Locale.defined thy (Locale.intern thy target)
    13.8 +  | init_target thy (SOME target) =
    13.9 +      if Locale.defined thy (Locale.intern thy target)
   13.10        then make_target target true (Class_Target.is_class thy target) ([], [], []) []
   13.11        else error ("No such locale: " ^ quote target);
   13.12