src/Pure/Isar/locale.ML

           ctxt |> fold (Variable.auto_fixes o #1) asms
           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
       in ((ctxt', Assumed axs), []) end
   | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
       ((ctxt, Derived ths), [])
-  | activate_elem _ is_ext ((ctxt, mode), Notes facts) =
+  | activate_elem _ is_ext ((ctxt, mode), Notes (kind, facts)) =
       let
         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
-        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i facts';
+        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
       in ((ctxt', mode), if is_ext then res else []) end;
 
 fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
     val ((ctxt', _), res) =
-        foldl_map (activate_elem ax_in_ctxt (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
-      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
+      foldl_map (activate_elem ax_in_ctxt (name = ""))
+        ((ProofContext.qualified_names ctxt, mode), elems)
+      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
     val ctxt'' = if name = "" then ctxt'
           else let
               val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
               val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
             in case mode of

   | declare_ext_elem prep_vars (ctxt, Constrains csts) =
       let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
       in (ctxt', []) end
   | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
   | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
-  | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
+  | declare_ext_elem _ (ctxt, Notes _) = (ctxt, []);
 
 fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
     let val (ctxt', propps) =
       (case elems of
         Int es => foldl_map declare_int_elem (ctxt, es)

 
   | finish_derived _ _ (Derived _) (Fixes _) = NONE
   | finish_derived _ _ (Derived _) (Constrains _) = NONE
   | finish_derived sign wits (Derived _) (Assumes asms) = asms
       |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
-      |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
+      |> pair Thm.assumptionK |> Notes
+      |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
   | finish_derived sign wits (Derived _) (Defines defs) = defs
       |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
-      |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
-
-  | finish_derived _ wits _ (Notes facts) = (Notes facts)
+      |> pair Thm.definitionK |> Notes
+      |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
+
+  | finish_derived _ wits _ (Notes facts) = Notes facts
       |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME;
 
 (* CB: for finish_elems (Ext) *)
 
 fun closeup _ false elem = elem

     val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
     val (import_ctxt, (import_elemss, _)) =
       activate_facts false prep_facts (context, ps);
 
     val (ctxt, (elemss, _)) =
-      activate_facts false prep_facts (import_ctxt, qs);
+      activate_facts false prep_facts (ProofContext.set_stmt true import_ctxt, qs);
   in
     ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
       (parms, spec, defs)), concl)
   end;
 

   |> Theory.qualified_names
   |> Theory.sticky_prefix prfx
   |> PureThy.note_thmss_i kind args
   ||> Theory.restore_naming thy;
 
-fun local_note_prefix_i prfx args ctxt =
+fun local_note_prefix_i kind prfx args ctxt =
   ctxt
   |> ProofContext.qualified_names
   |> ProofContext.sticky_prefix prfx
-  |> ProofContext.note_thmss_i args
+  |> ProofContext.note_thmss_i kind args
   ||> ProofContext.restore_naming ctxt;
 
 
 (* collect witnesses for global registration;
    requires parameters and flattened list of (assumed!) identifiers

 
 
 (* store instantiations of args for all registered interpretations
    of the theory *)
 
-fun note_thmss_registrations kind target args thy =
+fun note_thmss_registrations target (kind, args) thy =
   let
     val parms = the_locale thy target |> #params |> map fst;
     val ids = flatten (ProofContext.init thy, intern_expr thy)
       (([], Symtab.empty), Expr (Locale target)) |> fst |> fst
       |> map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE)

   #> (#2 o cert_context_statement (SOME loc) [] []);
 
 
 (* locale results *)
 
-fun add_thmss kind loc args ctxt =
+fun add_thmss loc kind args ctxt =
   let
     val (ctxt', ([(_, [Notes args'])], facts)) =
-      activate_facts true cert_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]);
+      activate_facts true cert_facts
+        (ctxt, [((("", []), Assumed []), [Ext (Notes (kind, args))])]);
     val ctxt'' = ctxt' |> ProofContext.theory
       (change_locale loc
         (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
           (axiom, import, elems @ [(Notes args', stamp ())],
             params, lparams, term_syntax, regs, intros))
-      #> note_thmss_registrations kind loc args');
+      #> note_thmss_registrations loc args');
   in (facts, ctxt'') end;
 
 
 
 (** define locales **)

        (Tactic.rewrite_goals_tac defs THEN
         Tactic.compose_tac (false, ax, 0) 1));
   in ((statement, intro, axioms), defs_thy) end;
 
 fun assumes_to_notes (Assumes asms) axms =
-    fold_map (fn (a, spec) => fn axs =>
-       let val (ps, qs) = chop (length spec) axs
-       in ((a, [(ps, [])]), qs) end) asms axms
-    |> apfst Notes
+      fold_map (fn (a, spec) => fn axs =>
+          let val (ps, qs) = chop (length spec) axs
+          in ((a, [(ps, [])]), qs) end) asms axms
+      |> apfst (curry Notes Thm.assumptionK)
   | assumes_to_notes e axms = (e, axms);
 
 (* CB: the following two change only "new" elems, these have identifier ("", _). *)
 
 (* turn Assumes into Notes elements *)

 (* adjust hyps of Notes elements *)
 
 fun change_elemss_hyps axioms elemss =
   let
     fun change (id as ("", _), es) =
-        (id, map (fn e as (Notes _) => Element.map_ctxt_values I I (Element.satisfy_thm axioms) e
+        (id, map (fn e as Notes _ => Element.map_ctxt_values I I (Element.satisfy_thm axioms) e
                    | e => e) es)
       | change e = e;
   in map change elemss end;
 
 in

           val aname = if null ints then bname else bname ^ "_" ^ axiomsN;
           val ((statement, intro, axioms), def_thy) =
             thy |> def_pred aname parms defs exts exts';
           val elemss' = change_assumes_elemss axioms elemss;
           val def_thy' = def_thy
-            |> PureThy.note_thmss_qualified "" aname [((introN, []), [([intro], [])])]
+            |> PureThy.note_thmss_qualified Thm.definitionK
+              aname [((introN, []), [([intro], [])])]
             |> snd;
           val a_elem = [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
         in ((elemss', [statement]), a_elem, [intro], def_thy') end;
     val (predicate, stmt', elemss'', b_intro, thy'') =
       if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy')

             thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
           val cstatement = Thm.cterm_of def_thy statement;
           val elemss'' = change_elemss_hyps axioms elemss';
           val def_thy' =
           def_thy
-          |> PureThy.note_thmss_qualified "" bname
-               [((introN, []), [([intro], [])]),
+          |> PureThy.note_thmss_qualified Thm.definitionK bname
+              [((introN, []), [([intro], [])]),
                 ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
           |> snd;
           val b_elem = [(("", []),
                [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
         in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], def_thy') end;

 fun defines_to_notes is_ext thy (Defines defs) defns =
     let
       val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
       val notes = map (fn (a, (def, _)) =>
         (a, [([assume (cterm_of thy def)], [])])) defs
-    in (if is_ext then SOME (Notes notes) else NONE, defns @ [Defines defs']) end
+    in
+      (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs'])
+    end
   | defines_to_notes _ _ e defns = (SOME e, defns);
 
 fun change_defines_elemss thy elemss defns =
   let
     fun change (id as (n, _), es) defns =

     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
     val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
     val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
     val axs' = map (Element.assume_witness pred_thy) stmt';
     val loc_ctxt = pred_thy
-      |> PureThy.note_thmss_qualified "" bname facts' |> snd
+      |> PureThy.note_thmss_qualified Thm.assumptionK bname facts' |> snd
       |> declare_locale name
       |> put_locale name
        {axiom = axs',
         import = import,
         elems = map (fn e => (e, stamp ())) elems'',

 (* activate instantiated facts in theory or context *)
 
 fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit
         attn all_elemss new_elemss propss thmss thy_ctxt =
     let
-      fun activate_elem disch (prfx, atts) (Notes facts) thy_ctxt =
+      fun activate_elem disch (prfx, atts) (Notes (kind, facts)) thy_ctxt =
           let
             val facts' = facts
               (* discharge hyps in attributes *)
               |> Attrib.map_facts (attrib thy_ctxt o Args.map_values I I I disch)
-              (* insert interpretation attributes *)
+              (* append interpretation attributes *)
               |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
               (* discharge hyps *)
               |> map (apsnd (map (apfst (map disch))));
-          in snd (note prfx facts' thy_ctxt) end
+          in snd (note kind prfx facts' thy_ctxt) end
         | activate_elem _ _ _ thy_ctxt = thy_ctxt;
 
       fun activate_elems disch ((id, _), elems) thy_ctxt =
           let
             val ((prfx, atts2), _) = the (get_reg thy_ctxt id)

     end;
 
 fun global_activate_facts_elemss x = gen_activate_facts_elemss
       (fn thy => fn (name, ps) =>
         get_global_registration thy (name, map Logic.varify ps))
-      (global_note_prefix_i "")
+      global_note_prefix_i
       Attrib.attribute_i Drule.standard
       (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
       (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
         Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, legacy_unvarify th))
         (* FIXME *)) x;

                        (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
                        (Element.inst_term insts t,
                         disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
               end;
 
-            fun activate_elem (Notes facts) thy =
+            fun activate_elem (Notes (kind, facts)) thy =
                 let
                   val facts' = facts
                       |> Attrib.map_facts (Attrib.attribute_i thy o
                          Args.map_values I (Element.instT_type (#1 insts))
                            (Element.inst_term insts)
                            (disch o Element.inst_thm thy insts o satisfy))
                       |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
                       |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
                 in
                   thy
-                  |> global_note_prefix_i "" prfx facts'
+                  |> global_note_prefix_i kind prfx facts'
                   |> snd
                 end
               | activate_elem _ thy = thy;
 
             fun activate_elems (_, elems) thy = fold activate_elem elems thy;

     fun after_qed' results =
       ProofContext.theory (activate (prep_result propss results))
       #> after_qed;
   in
     ProofContext.init thy
-    |> Proof.theorem_i "interpretation" NONE after_qed' (prep_propp propss)
+    |> Proof.theorem_i NONE after_qed' (prep_propp propss)
     |> Element.refine_witness |> Seq.hd
   end;
 
 fun interpretation_in_locale after_qed (raw_target, expr) thy =
   let

     fun after_qed' results =
       ProofContext.theory (activate (prep_result propss results))
       #> after_qed;
   in
     goal_ctxt
-    |> Proof.theorem_i "interpretation" NONE after_qed' propp
+    |> Proof.theorem_i NONE after_qed' propp
     |> Element.refine_witness |> Seq.hd
   end;
 
 fun interpret after_qed (prfx, atts) expr insts int state =
   let