# HG changeset patch
# User wenzelm
# Date 1164128849 -3600
# Node ID 89104dca628efeed56d8973cca4c04c70c8bc3d0
# Parent  625797c592b2ccb4705511a49c866a2d9beb4efd
LocalTheory.axioms/notes/defs: proper kind;
context_notes: ProofContext.set_stmt after import;

diff -r 625797c592b2 -r 89104dca628e src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Nov 21 12:55:39 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Tue Nov 21 18:07:29 2006 +0100
@@ -157,6 +157,9 @@
 fun message s = if ! quiet_mode then () else writeln s;
 fun clean_message s = if ! quick_and_dirty then () else message s;
 
+val note_theorems = LocalTheory.notes Thm.theoremK;
+val note_theorem = LocalTheory.note Thm.theoremK;
+
 fun coind_prefix true = "co"
   | coind_prefix false = "";
 
@@ -416,7 +419,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 |> note_theorems facts |>> map snd end;
 
 val inductive_cases = gen_inductive_cases Attrib.intern_src ProofContext.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
@@ -591,7 +594,7 @@
     val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
       Variable.add_fixes (map (fst o dest_Free) params) |> snd |>
       fold Variable.declare_term intr_ts |>
-      LocalTheory.def
+      LocalTheory.def Thm.internalK
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
          (("", []), fold_rev lambda params
            (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
@@ -608,7 +611,7 @@
             (list_comb (rec_const, params @ make_bool_args' bs i @
               make_args argTs (xs ~~ Ts)))))
         end) (cnames_syn ~~ cs);
-    val (consts_defs, ctxt'') = fold_map LocalTheory.def specs ctxt';
+    val (consts_defs, ctxt'') = fold_map (LocalTheory.def Thm.internalK) specs ctxt';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
     val mono = prove_mono predT fp_fun monos ctxt''
@@ -657,23 +660,23 @@
 
     val (intrs', ctxt2) =
       ctxt1 |>
-      LocalTheory.notes
+      note_theorems
         (map (NameSpace.qualified rec_name) intr_names ~~
          intr_atts ~~
          map (fn th => [([th], [])]) (ProofContext.export ctxt1 ctxt intrs)) |>>
       map (hd o snd); (* FIXME? *)
     val (((_, elims'), (_, [induct'])), ctxt3) =
       ctxt2 |>
-      LocalTheory.note ((NameSpace.qualified rec_name "intros",
+      note_theorem ((NameSpace.qualified rec_name "intros",
           [Attrib.internal (ContextRules.intro_query NONE)]), intrs') ||>>
       fold_map (fn (name, (elim, cases)) =>
-        LocalTheory.note ((NameSpace.qualified (Sign.base_name name) "cases",
+        note_theorem ((NameSpace.qualified (Sign.base_name name) "cases",
           [Attrib.internal (RuleCases.case_names cases),
            Attrib.internal (RuleCases.consumes 1),
            Attrib.internal (InductAttrib.cases_set name),
            Attrib.internal (ContextRules.elim_query NONE)]), [elim]) #>
         apfst (hd o snd)) elims ||>>
-      LocalTheory.note ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
+      note_theorem ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
         map Attrib.internal (#2 induct)), [rulify (#1 induct)]);
 
     val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
@@ -681,11 +684,11 @@
       let val inducts = cnames ~~ ProjectRule.projects ctxt (1 upto length cnames) induct'
       in
         ctxt3 |>
-        LocalTheory.notes (inducts |> map (fn (name, th) => (("",
+        note_theorems (inducts |> map (fn (name, th) => (("",
           [Attrib.internal ind_case_names,
            Attrib.internal (RuleCases.consumes 1),
            Attrib.internal (induct_att name)]), [([th], [])]))) |> snd |>
-        LocalTheory.note ((NameSpace.qualified rec_name (coind_prefix coind ^ "inducts"),
+        note_theorem ((NameSpace.qualified rec_name (coind_prefix coind ^ "inducts"),
           [Attrib.internal ind_case_names,
            Attrib.internal (RuleCases.consumes 1)]), map snd inducts) |> snd
       end;
diff -r 625797c592b2 -r 89104dca628e src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Nov 21 12:55:39 2006 +0100
+++ b/src/Pure/Isar/local_theory.ML	Tue Nov 21 18:07:29 2006 +0100
@@ -21,17 +21,17 @@
   val pretty: local_theory -> Pretty.T list
   val consts: (string * typ -> bool) ->
     ((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory
-  val axioms: ((bstring * Attrib.src list) * term list) list -> local_theory ->
+  val axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory ->
     (bstring * thm list) list * local_theory
-  val defs: ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list ->
+  val defs: string -> ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list ->
     local_theory -> (term * (bstring * thm)) list * local_theory
-  val notes: ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+  val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     local_theory -> (bstring * thm list) list * local_theory
   val term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory
   val declaration: (Context.generic -> Context.generic) -> local_theory -> local_theory
-  val def: (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
+  val def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
     local_theory -> (term * (bstring * thm)) * local_theory
-  val note: (bstring * Attrib.src list) * thm list ->
+  val note: string -> (bstring * Attrib.src list) * thm list ->
     local_theory -> (bstring * thm list) * Proof.context
   val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> local_theory ->
@@ -53,12 +53,13 @@
  {pretty: local_theory -> Pretty.T list,
   consts: (string * typ -> bool) -> ((bstring * typ) * mixfix) list -> local_theory ->
     (term * thm) list * local_theory,
-  axioms: ((bstring * Attrib.src list) * term list) list -> local_theory ->
+  axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory ->
     (bstring * thm list) list * local_theory,
-  defs: ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list -> local_theory ->
-    (term * (bstring * thm)) list * local_theory,
-  notes: ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> local_theory ->
-    (bstring * thm list) list * local_theory,
+  defs: string -> ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list ->
+    local_theory -> (term * (bstring * thm)) list * local_theory,
+  notes: string ->
+    ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+    local_theory -> (bstring * thm list) list * local_theory,
   term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory,
   declaration: (Context.generic -> Context.generic) -> local_theory -> local_theory,
   reinit: local_theory -> theory -> local_theory,
@@ -143,18 +144,18 @@
 
 val pretty = operation #pretty;
 val consts = operation2 #consts;
-val axioms = operation1 #axioms;
-val defs = operation1 #defs;
-val notes = operation1 #notes;
+val axioms = operation2 #axioms;
+val defs = operation2 #defs;
+val notes = operation2 #notes;
 val term_syntax = operation1 #term_syntax;
 val declaration = operation1 #declaration;
 
 
 (* derived operations *)
 
-fun def arg lthy = lthy |> defs [arg] |>> hd;
+fun def kind arg lthy = lthy |> defs kind [arg] |>> hd;
 
-fun note (a, ths) lthy = lthy |> notes [(a, [(ths, [])])] |>> hd;
+fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd;
 
 fun notation mode args = term_syntax
   (Context.mapping (Sign.add_notation mode args) (ProofContext.add_notation mode args));
diff -r 625797c592b2 -r 89104dca628e src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Nov 21 12:55:39 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Tue Nov 21 18:07:29 2006 +0100
@@ -97,7 +97,7 @@
 
 in
 
-fun axioms specs lthy =
+fun axioms kind specs lthy =
   let
     val hyps = Assumption.assms_of lthy;
     fun axiom ((name, atts), props) thy = thy
@@ -107,7 +107,7 @@
     lthy
     |> fold (fold Variable.declare_term o snd) specs
     |> LocalTheory.theory_result (fold_map axiom specs)
-    |-> LocalTheory.notes
+    |-> LocalTheory.notes kind
   end;
 
 end;
@@ -127,7 +127,7 @@
 
 in
 
-fun defs args lthy =
+fun defs kind args lthy =
   let
     fun def ((x, mx), ((name, atts), rhs)) lthy1 =
       let
@@ -152,7 +152,7 @@
       in ((lhs, ((name', atts), [([eq], [])])), lthy3) end;
 
     val ((lhss, facts), lthy') = lthy |> fold_map def args |>> split_list;
-    val (res, lthy'') = lthy' |> LocalTheory.notes facts;
+    val (res, lthy'') = lthy' |> LocalTheory.notes kind facts;
   in (lhss ~~ map (apsnd the_single) res, lthy'') end;
 
 end;
@@ -160,19 +160,21 @@
 
 (* notes *)
 
-fun context_notes facts lthy =
+fun context_notes kind facts lthy =
   let
     val facts' = facts
       |> Element.export_standard_facts lthy lthy
       |> Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of lthy));
   in
     lthy
+    |> ProofContext.set_stmt true
     |> ProofContext.qualified_names
-    |> ProofContext.note_thmss_i facts'
+    |> ProofContext.note_thmss_i kind facts'
     ||> ProofContext.restore_naming lthy
+    ||> ProofContext.restore_stmt lthy
   end;
 
-fun theory_notes keep_atts facts lthy = lthy |> LocalTheory.theory (fn thy =>
+fun theory_notes keep_atts kind facts lthy = lthy |> LocalTheory.theory (fn thy =>
   let
     val facts' = facts
       |> Element.export_standard_facts lthy (ProofContext.init thy)
@@ -180,15 +182,16 @@
   in
     thy
     |> Sign.qualified_names
-    |> PureThy.note_thmss_i "" facts' |> #2
+    |> PureThy.note_thmss_i kind facts' |> #2
     |> Sign.restore_naming thy
   end);
 
-fun locale_notes loc facts lthy = lthy |> LocalTheory.target (fn ctxt =>
-  #2 (Locale.add_thmss "" loc (Element.export_standard_facts lthy ctxt facts) ctxt));
+fun locale_notes loc kind facts lthy = lthy |> LocalTheory.target (fn ctxt =>
+  #2 (Locale.add_thmss loc kind (Element.export_standard_facts lthy ctxt facts) ctxt));
 
-fun notes "" facts = theory_notes true facts #> context_notes facts
-  | notes loc facts = theory_notes false facts #> locale_notes loc facts #> context_notes facts;
+fun notes "" kind facts = theory_notes true kind facts #> context_notes kind facts
+  | notes loc kind facts = theory_notes false kind facts #>
+      locale_notes loc kind facts #> context_notes kind facts;
 
 
 (* declarations *)