# HG changeset patch
# User wenzelm
# Date 1165277852 -3600
# Node ID c8a0370c9b9353c1de476c73f1a3630a5239971d
# Parent  fccafa917a680a941ccd9feff0c518d377137825
more careful indexing of local facts;

diff -r fccafa917a68 -r c8a0370c9b93 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Dec 05 00:42:36 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Dec 05 01:17:32 2006 +0100
@@ -766,25 +766,25 @@
 (* put_thms *)
 
 fun update_thms _ ("", NONE) ctxt = ctxt
-  | update_thms do_index ("", SOME ths) ctxt = ctxt |> map_thms (fn (facts, index) =>
+  | update_thms opts ("", SOME ths) ctxt = ctxt |> map_thms (fn (facts, index) =>
       let
-        val index' = FactIndex.add_local do_index ("", ths) index;
+        val index' = uncurry FactIndex.add_local opts ("", ths) index;
       in (facts, index') end)
   | 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)
-  | update_thms do_index (bname, SOME ths) ctxt = ctxt |> map_thms (fn ((space, tab), index) =>
+  | update_thms opts (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;
         val tab' = Symtab.update (name, ths) tab;
-        val index' = FactIndex.add_local do_index (name, ths) index;
+        val index' = uncurry FactIndex.add_local opts (name, ths) index;
       in ((space', tab'), index') end);
 
 fun put_thms thms ctxt =
-  ctxt |> map_naming (K local_naming) |> update_thms false thms |> restore_naming ctxt;
+  ctxt |> map_naming (K local_naming) |> update_thms (true, false) thms |> restore_naming ctxt;
 
 
 (* note_thmss *)
@@ -799,7 +799,7 @@
       swap (foldl_map (Thm.proof_attributes (attrs @ more_attrs @ [PureThy.kind k])) (x, th));
     val (res, ctxt') = fold_map app facts ctxt;
     val thms = PureThy.name_thms false false name (flat res);
-  in ((bname, thms), ctxt' |> update_thms (is_stmt ctxt) (bname, SOME thms)) end);
+  in ((bname, thms), ctxt' |> update_thms (is_stmt ctxt, true) (bname, SOME thms)) end);
 
 in
 
diff -r fccafa917a68 -r c8a0370c9b93 src/Pure/fact_index.ML
--- a/src/Pure/fact_index.ML	Tue Dec 05 00:42:36 2006 +0100
+++ b/src/Pure/fact_index.ML	Tue Dec 05 01:17:32 2006 +0100
@@ -13,8 +13,8 @@
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val empty: T
+  val add_local: bool -> bool -> (string * thm list) -> T -> T
   val add_global: (string * thm list) -> T -> T
-  val add_local: bool -> (string * thm list) -> T -> T
   val find: T -> spec -> (string * thm list) list
 end;
 
@@ -59,7 +59,7 @@
 val empty =
   Index {facts = [], consts = Symtab.empty, frees = Symtab.empty, props = Net.empty};
 
-fun add do_props do_index (fact as (_, ths)) (Index {facts, consts, frees, props}) =
+fun add_local do_props do_index (fact as (_, ths)) (Index {facts, consts, frees, props}) =
   let
     val entry = (serial (), fact);
     val (cs, xs) = fold index_thm ths ([], []);
@@ -75,8 +75,7 @@
       else props;
   in Index {facts = facts', consts = consts', frees = frees', props = props'} end;
 
-val add_global = add false true;
-val add_local = add true;
+val add_global = add_local false true;
 
 
 (* find by consts/frees *)