eliminated slightly odd kind argument of LocalTheory.note(s);
added LocalTheory.notes_kind as fall-back for unusual cases;

--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -561,20 +561,19 @@
             (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
           else (strong_raw_induct RSN (2, rev_mp),
             [ind_case_names, Rule_Cases.consumes 1]);
-        val ((_, [strong_induct']), ctxt') = LocalTheory.note ""
+        val ((_, [strong_induct']), ctxt') = ctxt |> LocalTheory.note
           ((rec_qualified (Binding.name "strong_induct"),
-            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
-          ctxt;
+            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
         val strong_inducts =
-          Project_Rule.projects ctxt (1 upto length names) strong_induct'
+          Project_Rule.projects ctxt (1 upto length names) strong_induct';
       in
         ctxt' |>
-        LocalTheory.note ""
+        LocalTheory.note
           ((rec_qualified (Binding.name "strong_inducts"),
             [Attrib.internal (K ind_case_names),
              Attrib.internal (K (Rule_Cases.consumes 1))]),
            strong_inducts) |> snd |>
-        LocalTheory.notes "" (map (fn ((name, elim), (_, cases)) =>
+        LocalTheory.notes (map (fn ((name, elim), (_, cases)) =>
             ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
               [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
                Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
@@ -664,7 +663,7 @@
       end) atoms
   in
     ctxt |>
-    LocalTheory.notes "" (map (fn (name, ths) =>
+    LocalTheory.notes (map (fn (name, ths) =>
         ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
           [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
       (names ~~ transp thss)) |> snd

--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -466,15 +466,14 @@
             NONE => (rec_qualified (Binding.name "strong_induct"),
                      rec_qualified (Binding.name "strong_inducts"))
           | SOME s => (Binding.name s, Binding.name (s ^ "s"));
-        val ((_, [strong_induct']), ctxt') = LocalTheory.note ""
+        val ((_, [strong_induct']), ctxt') = ctxt |> LocalTheory.note
           ((induct_name,
-            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
-          ctxt;
+            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
         val strong_inducts =
           Project_Rule.projects ctxt' (1 upto length names) strong_induct'
       in
         ctxt' |>
-        LocalTheory.note ""
+        LocalTheory.note
           ((inducts_name,
             [Attrib.internal (K ind_case_names),
              Attrib.internal (K (Rule_Cases.consumes 1))]),

--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -367,11 +367,10 @@
       (fn thss => fn goal_ctxt =>
          let
            val simps = ProofContext.export goal_ctxt lthy' (flat thss);
-           val (simps', lthy'') = fold_map (LocalTheory.note "")
-             (names_atts' ~~ map single simps) lthy'
+           val (simps', lthy'') = fold_map LocalTheory.note (names_atts' ~~ map single simps) lthy';
          in
            lthy''
-           |> LocalTheory.note "" ((qualify (Binding.name "simps"),
+           |> LocalTheory.note ((qualify (Binding.name "simps"),
                 map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
                 maps snd simps')
            |> snd

--- a/src/HOL/Tools/Function/function.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -43,9 +43,6 @@
     [Simplifier.simp_add,
      Nitpick_Psimps.add]
 
-fun note_theorem ((binding, atts), ths) =
-  LocalTheory.note "" ((binding, atts), ths)
-
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
 
 fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy =
@@ -55,13 +52,13 @@
                    |> map (apfst (apfst extra_qualify))
 
       val (saved_spec_simps, lthy) =
-        fold_map (LocalTheory.note "") spec lthy
+        fold_map LocalTheory.note spec lthy
 
       val saved_simps = maps snd saved_spec_simps
       val simps_by_f = sort saved_simps
 
       fun add_for_f fname simps =
-        note_theorem ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
+        LocalTheory.note ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
         #> snd
     in
       (saved_simps,
@@ -100,14 +97,14 @@
             |> addsmps (conceal_partial o Binding.qualify false "partial")
                  "psimps" conceal_partial psimp_attribs psimps
             ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
-            ||>> note_theorem ((conceal_partial (qualify "pinduct"),
+            ||>> LocalTheory.note ((conceal_partial (qualify "pinduct"),
                    [Attrib.internal (K (Rule_Cases.case_names cnames)),
                     Attrib.internal (K (Rule_Cases.consumes 1)),
                     Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
-            ||>> note_theorem ((Binding.conceal (qualify "termination"), []), [termination])
-            ||> (snd o note_theorem ((qualify "cases",
+            ||>> LocalTheory.note ((Binding.conceal (qualify "termination"), []), [termination])
+            ||> (snd o LocalTheory.note ((qualify "cases",
                    [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
-            ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
+            ||> fold_option (snd oo curry LocalTheory.note (qualify "domintros", [])) domintros
 
           val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
                                       pinducts=snd pinducts', termination=termination',
@@ -155,7 +152,7 @@
           in
             lthy
             |> add_simps I "simps" I simp_attribs tsimps |> snd
-            |> note_theorem
+            |> LocalTheory.note
                ((qualify "induct",
                  [Attrib.internal (K (Rule_Cases.case_names case_names))]),
                 tinduct) |> snd

--- a/src/HOL/Tools/inductive.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -469,7 +469,7 @@
     val facts = args |> map (fn ((a, atts), props) =>
       ((a, map (prep_att thy) atts),
         map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
-  in lthy |> LocalTheory.notes "" facts |>> map snd end;
+  in lthy |> LocalTheory.notes facts |>> map snd end;
 
 val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
@@ -695,7 +695,7 @@
 
     val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'';
     val ((_, [mono']), lthy''') =
-      LocalTheory.note "" (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
+      LocalTheory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
 
   in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
     list_comb (rec_const, params), preds, argTs, bs, xs)
@@ -719,7 +719,7 @@
 
     val (intrs', lthy1) =
       lthy |>
-      LocalTheory.notes ""
+      LocalTheory.notes
         (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
           map (fn th => [([th],
            [Attrib.internal (K (Context_Rules.intro_query NONE)),
@@ -727,16 +727,16 @@
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), lthy2) =
       lthy1 |>
-      LocalTheory.note "" ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
+      LocalTheory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
       fold_map (fn (name, (elim, cases)) =>
-        LocalTheory.note ""
+        LocalTheory.note
           ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
             [Attrib.internal (K (Rule_Cases.case_names cases)),
              Attrib.internal (K (Rule_Cases.consumes 1)),
              Attrib.internal (K (Induct.cases_pred name)),
              Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
         apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
-      LocalTheory.note ""
+      LocalTheory.note
         ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
           map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
 
@@ -745,7 +745,7 @@
       else
         let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in
           lthy2 |>
-          LocalTheory.notes "" [((rec_qualified true (Binding.name "inducts"), []),
+          LocalTheory.notes [((rec_qualified true (Binding.name "inducts"), []),
             inducts |> map (fn (name, th) => ([th],
               [Attrib.internal (K ind_case_names),
                Attrib.internal (K (Rule_Cases.consumes 1)),

--- a/src/HOL/Tools/inductive_set.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -505,7 +505,7 @@
             (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
               [def, mem_Collect_eq, split_conv]) 1))
         in
-          lthy |> LocalTheory.note "" ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
+          lthy |> LocalTheory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
             [Attrib.internal (K pred_set_conv_att)]),
               [conv_thm]) |> snd
         end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;

--- a/src/HOL/Tools/primrec.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -277,8 +277,8 @@
     lthy
     |> set_group ? LocalTheory.set_group (serial ())
     |> add_primrec_simple fixes (map snd spec)
-    |-> (fn (prefix, simps) => fold_map (LocalTheory.note "") (attr_bindings prefix ~~ simps)
-      #-> (fn simps' => LocalTheory.note "" (simp_attr_binding prefix, maps snd simps')))
+    |-> (fn (prefix, simps) => fold_map LocalTheory.note (attr_bindings prefix ~~ simps)
+      #-> (fn simps' => LocalTheory.note (simp_attr_binding prefix, maps snd simps')))
     |>> snd
   end;
 

--- a/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -214,7 +214,7 @@
     lthy
     |> random_aux_primrec_multi (name ^ prfx) proto_eqs
     |-> (fn proto_simps => prove_simps proto_simps)
-    |-> (fn simps => LocalTheory.note ""
+    |-> (fn simps => LocalTheory.note
       ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K)
           [Simplifier.simp_add, Nitpick_Simps.add]), simps))
     |> snd

--- a/src/HOLCF/Tools/fixrec.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -242,7 +242,7 @@
         ((thm_name, [src]), [thm])
       end;
     val (thmss, lthy'') = lthy'
-      |> fold_map (LocalTheory.note "") (induct_note :: map unfold_note unfold_thms);
+      |> fold_map LocalTheory.note (induct_note :: map unfold_note unfold_thms);
   in
     (lthy'', names, fixdef_thms, map snd unfold_thms)
   end;
@@ -464,7 +464,7 @@
       val simps2 : (Attrib.binding * thm list) list =
         map (apsnd (fn thm => [thm])) (flat simps);
       val (_, lthy'') = lthy'
-        |> fold_map (LocalTheory.note "") (simps1 @ simps2);
+        |> fold_map LocalTheory.note (simps1 @ simps2);
     in
       lthy''
     end

--- a/src/Pure/Isar/expression.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -775,7 +775,7 @@
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
       |> Theory_Target.init (SOME name)
-      |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
+      |> fold (fn (kind, facts) => LocalTheory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
 

--- a/src/Pure/Isar/local_theory.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -33,8 +33,10 @@
     (term * term) * local_theory
   val define: string -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
-  val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
-  val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
+  val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
+  val notes: (Attrib.binding * (thm list * Attrib.src list) list) list ->
+    local_theory -> (string * thm list) list * local_theory
+  val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory
   val type_syntax: bool -> declaration -> local_theory -> local_theory
   val term_syntax: bool -> declaration -> local_theory -> local_theory
@@ -186,12 +188,13 @@
 val pretty = operation #pretty;
 val abbrev = apsnd checkpoint ooo operation2 #abbrev;
 val define = apsnd checkpoint ooo operation2 #define;
-val notes = apsnd checkpoint ooo operation2 #notes;
+val notes_kind = apsnd checkpoint ooo operation2 #notes;
 val type_syntax = checkpoint ooo operation2 #type_syntax;
 val term_syntax = checkpoint ooo operation2 #term_syntax;
 val declaration = checkpoint ooo operation2 #declaration;
 
-fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
+val notes = notes_kind "";
+fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
 
 fun notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args

--- a/src/Pure/Isar/specification.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -208,10 +208,10 @@
     val th = prove lthy2 raw_th;
     val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
 
-    val ((def_name, [th']), lthy4) = lthy3
-      |> LocalTheory.note Thm.definitionK
-        ((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
-            Code.add_default_eqn_attrib :: atts), [th]);
+    val ([(def_name, [th'])], lthy4) = lthy3
+      |> LocalTheory.notes_kind Thm.definitionK
+        [((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
+            Code.add_default_eqn_attrib :: atts), [([th], [])])];
 
     val lhs' = Morphism.term (LocalTheory.target_morphism lthy4) lhs;
     val _ =
@@ -270,7 +270,7 @@
     val facts = raw_facts |> map (fn ((name, atts), bs) =>
       ((name, map attrib atts),
         bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
-    val (res, lthy') = lthy |> LocalTheory.notes kind facts;
+    val (res, lthy') = lthy |> LocalTheory.notes_kind kind facts;
     val _ = Proof_Display.print_results true lthy' ((kind, ""), res);
   in (res, lthy') end;
 
@@ -359,14 +359,15 @@
         burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results
       in
         lthy
-        |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
+        |> LocalTheory.notes_kind kind
+          (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
         |> (fn (res, lthy') =>
           if Binding.is_empty name andalso null atts then
             (Proof_Display.print_results true lthy' ((kind, ""), res); lthy')
           else
             let
               val ([(res_name, _)], lthy'') = lthy'
-                |> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
+                |> LocalTheory.notes_kind kind [((name, atts), [(maps #2 res, [])])];
               val _ = Proof_Display.print_results true lthy' ((kind, res_name), res);
             in lthy'' end)
         |> after_qed results'

--- a/src/Pure/Isar/theory_target.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -310,7 +310,8 @@
 local
 
 fun init_target _ NONE = global_target
-  | init_target thy (SOME target) = if Locale.defined thy (Locale.intern thy target)
+  | init_target thy (SOME target) =
+      if Locale.defined thy (Locale.intern thy target)
       then make_target target true (Class_Target.is_class thy target) ([], [], []) []
       else error ("No such locale: " ^ quote target);