# HG changeset patch
# User wenzelm
# Date 1164128861 -3600
# Node ID cc5095d57da4ed71ec1adf9a7092d2176b434248
# Parent  56e54a2afe695cd2a3448a13f1d8b8e2178a8ff9
added stmt mode, which affects naming/indexing of local facts;
renamed put_thms_internal to put_thms;
notes: proper name and kind (outside of proof body);
removed dead code;

diff -r 56e54a2afe69 -r cc5095d57da4 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Nov 21 18:07:40 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Nov 21 18:07:41 2006 +0100
@@ -16,6 +16,9 @@
   val const_syntax_name: Proof.context -> string -> string
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
+  val is_stmt: Proof.context -> bool
+  val set_stmt: bool -> Proof.context -> Proof.context
+  val restore_stmt: Proof.context -> Proof.context -> Proof.context
   val fact_index_of: Proof.context -> FactIndex.T
   val transfer: theory -> Proof.context -> Proof.context
   val theory: (theory -> theory) -> Proof.context -> Proof.context
@@ -104,12 +107,11 @@
   val sticky_prefix: string -> Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val hide_thms: bool -> string list -> Proof.context -> Proof.context
-  val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
-  val put_thms_internal: string * thm list option -> Proof.context -> Proof.context
-  val note_thmss:
+  val put_thms: string * thm list option -> Proof.context -> Proof.context
+  val note_thmss: string ->
     ((bstring * attribute list) * (thmref * attribute list) list) list ->
       Proof.context -> (bstring * thm list) list * Proof.context
-  val note_thmss_i:
+  val note_thmss_i: string ->
     ((bstring * attribute list) * (thm list * attribute list) list) list ->
       Proof.context -> (bstring * thm list) list * Proof.context
   val read_vars: (string * string option * mixfix) list -> Proof.context ->
@@ -168,14 +170,16 @@
 
 datatype ctxt =
   Ctxt of
-   {naming: NameSpace.naming,                     (*local naming conventions*)
+   {is_stmt: bool,                                (*inner statement mode*)
+    naming: NameSpace.naming,                     (*local naming conventions*)
     syntax: LocalSyntax.T,                        (*local syntax*)
     consts: Consts.T * Consts.T,                  (*global/local consts*)
     thms: thm list NameSpace.table * FactIndex.T, (*local thms*)
     cases: (string * (RuleCases.T * bool)) list}; (*local contexts*)
 
-fun make_ctxt (naming, syntax, consts, thms, cases) =
-  Ctxt {naming = naming, syntax = syntax, consts = consts, thms = thms, cases = cases};
+fun make_ctxt (is_stmt, naming, syntax, consts, thms, cases) =
+  Ctxt {is_stmt = is_stmt, naming = naming, syntax = syntax,
+    consts = consts, thms = thms, cases = cases};
 
 val local_naming = NameSpace.default_naming |> NameSpace.add_path "local";
 
@@ -184,7 +188,7 @@
   val name = "Isar/context";
   type T = ctxt;
   fun init thy =
-    make_ctxt (local_naming, LocalSyntax.init thy,
+    make_ctxt (false, local_naming, LocalSyntax.init thy,
       (Sign.consts_of thy, Sign.consts_of thy),
       (NameSpace.empty_table, FactIndex.empty), []);
   fun print _ _ = ();
@@ -195,28 +199,35 @@
 fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
 
 fun map_context f =
-  ContextData.map (fn Ctxt {naming, syntax, consts, thms, cases} =>
-    make_ctxt (f (naming, syntax, consts, thms, cases)));
+  ContextData.map (fn Ctxt {is_stmt, naming, syntax, consts, thms, cases} =>
+    make_ctxt (f (is_stmt, naming, syntax, consts, thms, cases)));
+
+fun set_stmt b =
+  map_context (fn (_, naming, syntax, consts, thms, cases) =>
+    (b, naming, syntax, consts, thms, cases));
 
 fun map_naming f =
-  map_context (fn (naming, syntax, consts, thms, cases) =>
-    (f naming, syntax, consts, thms, cases));
+  map_context (fn (is_stmt, naming, syntax, consts, thms, cases) =>
+    (is_stmt, f naming, syntax, consts, thms, cases));
 
 fun map_syntax f =
-  map_context (fn (naming, syntax, consts, thms, cases) =>
-    (naming, f syntax, consts, thms, cases));
+  map_context (fn (is_stmt, naming, syntax, consts, thms, cases) =>
+    (is_stmt, naming, f syntax, consts, thms, cases));
 
 fun map_consts f =
-  map_context (fn (naming, syntax, consts, thms, cases) =>
-    (naming, syntax, f consts, thms, cases));
+  map_context (fn (is_stmt, naming, syntax, consts, thms, cases) =>
+    (is_stmt, naming, syntax, f consts, thms, cases));
 
 fun map_thms f =
-  map_context (fn (naming, syntax, consts, thms, cases) =>
-    (naming, syntax, consts, f thms, cases));
+  map_context (fn (is_stmt, naming, syntax, consts, thms, cases) =>
+    (is_stmt, naming, syntax, consts, f thms, cases));
 
 fun map_cases f =
-  map_context (fn (naming, syntax, consts, thms, cases) =>
-    (naming, syntax, consts, thms, f cases));
+  map_context (fn (is_stmt, naming, syntax, consts, thms, cases) =>
+    (is_stmt, naming, syntax, consts, thms, f cases));
+
+val is_stmt = #is_stmt o rep_context;
+fun restore_stmt ctxt = set_stmt (is_stmt ctxt);
 
 val naming_of = #naming o rep_context;
 val full_name = NameSpace.full o naming_of;
@@ -755,17 +766,17 @@
 
 (* put_thms *)
 
-fun put_thms _ ("", NONE) ctxt = ctxt
-  | put_thms do_index ("", SOME ths) ctxt = ctxt |> map_thms (fn (facts, index) =>
+fun update_thms _ ("", NONE) ctxt = ctxt
+  | update_thms do_index ("", SOME ths) ctxt = ctxt |> map_thms (fn (facts, index) =>
       let
         val index' = FactIndex.add_local do_index ("", ths) index;
       in (facts, index') end)
-  | put_thms _ (bname, NONE) ctxt = ctxt |> map_thms (fn ((space, tab), index) =>
+  | update_thms _ (bname, NONE) ctxt = ctxt |> map_thms (fn ((space, tab), index) =>
       let
         val name = full_name ctxt bname;
         val tab' = Symtab.delete_safe name tab;
       in ((space, tab'), index) end)
-  | put_thms do_index (bname, SOME ths) ctxt = ctxt |> map_thms (fn ((space, tab), index) =>
+  | update_thms do_index (bname, SOME ths) ctxt = ctxt |> map_thms (fn ((space, tab), index) =>
       let
         val name = full_name ctxt bname;
         val space' = NameSpace.declare (naming_of ctxt) name space;
@@ -773,31 +784,35 @@
         val index' = FactIndex.add_local do_index (name, ths) index;
       in ((space', tab'), index') end);
 
-fun put_thms_internal thms ctxt =
-  ctxt |> map_naming (K local_naming) |> put_thms false thms |> restore_naming ctxt;
+fun put_thms thms ctxt =
+  ctxt |> map_naming (K local_naming) |> update_thms false thms |> restore_naming ctxt;
 
 
 (* note_thmss *)
 
 local
 
-fun gen_note_thmss get = fold_map (fn ((name, more_attrs), ths_attrs) => fn ctxt =>
+fun gen_note_thmss get k = fold_map (fn ((bname, more_attrs), raw_facts) => fn ctxt =>
   let
-    fun app (th, attrs) (ct, ths) =
-      let val (ct', th') = foldl_map (Thm.proof_attributes (attrs @ more_attrs)) (ct, get ctxt th)
-      in (ct', th' :: ths) end;
-    val (ctxt', rev_thms) = fold app ths_attrs (ctxt, []);
-    val thms = flat (rev rev_thms);
-  in ((name, thms), ctxt' |> put_thms true (name, SOME thms)) end);
+    val name = full_name ctxt bname;
+    val stmt = is_stmt ctxt;
+
+    val kind = if stmt then [] else [PureThy.kind k];
+    val facts = raw_facts |> map (apfst (get ctxt))
+      |> (if stmt then I else PureThy.name_thmss name);
+
+    fun app (th, attrs) x =
+      swap (foldl_map (Thm.proof_attributes (attrs @ more_attrs @ kind)) (x, th));
+    val (res, ctxt') = fold_map app facts ctxt;
+    val thms = flat res
+      |> (if stmt then I else PureThy.name_thms false name);
+  in ((bname, thms), ctxt' |> update_thms stmt (bname, SOME thms)) end);
 
 in
 
 val note_thmss = gen_note_thmss get_thms;
 val note_thmss_i = gen_note_thmss (K I);
 
-val note_thmss_accesses = gen_note_thmss get_thms;
-val note_thmss_accesses_i = gen_note_thmss (K I);
-
 end;
 
 
@@ -950,8 +965,8 @@
   in
     ctxt2
     |> auto_bind_facts (flat propss)
-    |> put_thms_internal (AutoBind.premsN, SOME (Assumption.prems_of ctxt2))
-    |> note_thmss_i (map fst args ~~ map (map (fn th => ([th], []))) premss)
+    |> put_thms (AutoBind.premsN, SOME (Assumption.prems_of ctxt2))
+    |> note_thmss_i Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
   end;
 
 in