src/Pure/Isar/locale.ML

   val print_locales: theory -> unit
   val print_locale: theory -> expr -> context attribute element list -> unit
   val add_locale: bool -> bstring -> expr -> context attribute element list -> theory -> theory
   val add_locale_i: bool -> bstring -> expr -> context attribute element_i list
     -> theory -> theory
-  val smart_have_thmss: string -> (string * 'a) Library.option ->
+  val smart_note_thmss: string -> (string * 'a) Library.option ->
     ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
-  val have_thmss: string -> xstring ->
+  val note_thmss: string -> xstring ->
     ((bstring * context attribute list) * (xstring * context attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
-  val have_thmss_i: string -> string ->
+  val note_thmss_i: string -> string ->
     ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
   val add_thmss: string -> ((string * thm list) * context attribute list) list ->
     theory * context -> (theory * context) * (string * thm list) list
   val prune_prems: theory -> thm -> thm

           (defs |> map (fn ((name, atts), (t, ps)) =>
             let val (c, t') = ProofContext.cert_def ctxt t
             in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
       in ((ctxt', axs), []) end
   | activate_elem is_ext ((ctxt, axs), Notes facts) =
-      let val (ctxt', res) = ctxt |> ProofContext.have_thmss_i facts
+      let val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts
       in ((ctxt', axs), if is_ext then res else []) end;
 
 fun activate_elems ((name, ps), elems) (ctxt, axs) =
   let val ((ctxt', axs'), res) =
     foldl_map (activate_elem (name = "")) ((ProofContext.qualified true ctxt, axs), elems)

 		  cat_lines (map string_of_thm thms))
               (* rename fact *)
               val facts'' = map (apfst (apfst prefix_fact)) facts'
               (* add attributes *)
               val facts''' = map (apfst (apsnd (fn atts => atts @ attribs))) facts''
-          in fst (ProofContext.have_thmss_i facts''' ctxt)
+          in fst (ProofContext.note_thmss_i facts''' ctxt)
           end
       | inst_elem (ctxt, (Int _)) = ctxt;
 
     fun inst_elems (ctxt, (id, elems)) = foldl inst_elem (ctxt, elems);
 

   thy |> PureThy.hide_thms false
     (map (Sign.full_name (Theory.sign_of thy)) (filter_out (equal "") names));
 
 in
 
-fun have_thmss_qualified kind name args thy =
+fun note_thmss_qualified kind name args thy =
   thy
   |> Theory.add_path (Sign.base_name name)
-  |> PureThy.have_thmss_i (Drule.kind kind) args
+  |> PureThy.note_thmss_i (Drule.kind kind) args
   |>> hide_bound_names (map (#1 o #1) args)
   |>> Theory.parent_path;
 
-fun smart_have_thmss kind None = PureThy.have_thmss_i (Drule.kind kind)
-  | smart_have_thmss kind (Some (loc, _)) = have_thmss_qualified kind loc;
+fun smart_note_thmss kind None = PureThy.note_thmss_i (Drule.kind kind)
+  | smart_note_thmss kind (Some (loc, _)) = note_thmss_qualified kind loc;
   (* CB: only used in Proof.finish_global. *)
 
 end;
 
 local

     val {view, import, elems, params} = the_locale thy loc;
     val note = Notes (map (fn ((a, more_atts), th_atts) =>
       ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args);
   in thy |> put_locale loc (make_locale view import (elems @ [(note, stamp ())]) params) end;
 
-fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy =
+fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy =
   let
     val thy_ctxt = ProofContext.init thy;
     val loc = prep_locale (Theory.sign_of thy) raw_loc;
     val (_, view, loc_ctxt, _, _) = cert_context_statement (Some loc) [] [] thy_ctxt;
     val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args;
     val export = ProofContext.export_standard view loc_ctxt thy_ctxt;
-    val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt));
+    val results = map (map export o #2) (#2 (ProofContext.note_thmss_i args loc_ctxt));
     val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results;
   in
     thy
     |> put_facts loc args
-    |> have_thmss_qualified kind loc args'
+    |> note_thmss_qualified kind loc args'
   end;
 
 in
 
-val have_thmss = gen_have_thmss intern ProofContext.get_thms;
-val have_thmss_i = gen_have_thmss (K I) (K I);
-  (* CB: have_thmss(_i) is the base for the Isar commands
+val note_thmss = gen_note_thmss intern ProofContext.get_thms;
+val note_thmss_i = gen_note_thmss (K I) (K I);
+  (* CB: note_thmss(_i) is the base for the Isar commands
      "theorems (in loc)" and "declare (in loc)". *)
 
 fun add_thmss loc args (thy, ctxt) =
   let
     val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;

           val (def_thy, (statement, intro, axioms)) =
             thy |> def_pred aname parms defs exts exts';
           val elemss' = change_elemss axioms elemss @
             [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
         in
-          def_thy |> have_thmss_qualified "" aname
+          def_thy |> note_thmss_qualified "" aname
             [((introN, []), [([intro], [])])]
           |> #1 |> rpair (elemss', [statement])
         end;
     val (thy'', view) =
       if Library.null ints then (thy', ([], []))

         let
           val (def_thy, (statement, intro, axioms)) =
             thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
           val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement;
         in
-          def_thy |> have_thmss_qualified "" bname
+          def_thy |> note_thmss_qualified "" bname
             [((introN, []), [([intro], [])]),
              ((axiomsN, []), [(map Drule.standard axioms, [])])]
           |> #1 |> rpair ([cstatement], axioms)
         end;
   in (thy'', (elemss', view)) end;

     val ((ctxt, _), (_, facts)) = activate_facts (K I) ((pred_ctxt, view_axioms), elemss');
     val export = ProofContext.export_standard view_statement ctxt pred_ctxt;
     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
   in
     pred_thy
-    |> have_thmss_qualified "" name facts' |> #1
+    |> note_thmss_qualified "" name facts' |> #1
     |> declare_locale name
     |> put_locale name (make_locale view (prep_expr sign raw_import)
         (map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss'))))
         (params_of elemss', map #1 (params_of body_elemss)))
   end;