# HG changeset patch
# User wenzelm
# Date 1164128858 -3600
# Node ID 940ef3e85c5a77d2cba85e2ed8ef31e5c38e107f
# Parent  807a39221a58b75ddd5cf737b51fe7dccc0c576e
notes: proper kind;
simplified Proof.theorem(_i);
context_statement: ProofContext.set_stmt after import;

diff -r 807a39221a58 -r 940ef3e85c5a src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Nov 21 18:07:37 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Nov 21 18:07:38 2006 +0100
@@ -886,18 +886,19 @@
       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;
@@ -1005,7 +1006,7 @@
       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) =
@@ -1093,12 +1094,14 @@
   | 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
+      |> pair Thm.definitionK |> Notes
+      |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
 
-  | finish_derived _ wits _ (Notes facts) = (Notes facts)
+  | finish_derived _ wits _ (Notes facts) = Notes facts
       |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME;
 
 (* CB: for finish_elems (Ext) *)
@@ -1390,7 +1393,7 @@
       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)
@@ -1457,11 +1460,11 @@
   |> 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;
 
 
@@ -1488,7 +1491,7 @@
 (* 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)
@@ -1535,16 +1538,17 @@
 
 (* 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;
 
 
@@ -1629,10 +1633,10 @@
   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 ("", _). *)
@@ -1655,7 +1659,7 @@
 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;
@@ -1675,7 +1679,8 @@
             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;
@@ -1689,8 +1694,8 @@
           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 = [(("", []),
@@ -1712,7 +1717,9 @@
       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 =
@@ -1778,7 +1785,7 @@
     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',
@@ -1871,16 +1878,16 @@
 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 =
@@ -1917,7 +1924,7 @@
 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
@@ -2114,7 +2121,7 @@
                         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
@@ -2125,7 +2132,7 @@
                       |> 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;
@@ -2158,7 +2165,7 @@
       #> 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;
 
@@ -2177,7 +2184,7 @@
       #> 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;