more explicit flags for facts table;

--- a/src/Pure/Isar/proof_context.ML	Tue Oct 09 15:31:45 2012 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 09 19:24:19 2012 +0200
@@ -938,8 +938,8 @@
 local
 
 fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
-  | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
-      (Facts.add_local (Context.Proof ctxt) do_props (b, ths) #> snd);
+  | update_thms flags (b, SOME ths) ctxt = ctxt |> map_facts
+      (Facts.add_static (Context.Proof ctxt) flags (b, ths) #> snd);
 
 in
 
@@ -952,12 +952,12 @@
     val (res, ctxt') = fold_map app facts ctxt;
     val thms = Global_Theory.name_thms false false name (flat res);
     val Mode {stmt, ...} = get_mode ctxt;
-  in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
+  in ((name, thms), ctxt' |> update_thms {strict = false, index = stmt} (b, SOME thms)) end);
 
-fun put_thms do_props thms ctxt = ctxt
+fun put_thms index thms ctxt = ctxt
   |> map_naming (K Name_Space.local_naming)
   |> Context_Position.set_visible false
-  |> update_thms do_props (apfst Binding.name thms)
+  |> update_thms {strict = false, index = index} (apfst Binding.name thms)
   |> Context_Position.restore_visible ctxt
   |> restore_naming ctxt;
 

--- a/src/Pure/facts.ML	Tue Oct 09 15:31:45 2012 +0200
+++ b/src/Pure/facts.ML	Tue Oct 09 19:24:19 2012 +0200
@@ -32,8 +32,8 @@
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val merge: T * T -> T
-  val add_global: Context.generic -> binding * thm list -> T -> string * T
-  val add_local: Context.generic -> bool -> binding * thm list -> T -> string * T
+  val add_static: Context.generic -> {strict: bool, index: bool} ->
+    binding * thm list -> T -> string * T
   val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
   val del: string -> T -> T
   val hide: bool -> string -> T -> T
@@ -188,26 +188,15 @@
 
 (* add static entries *)
 
-local
-
-fun add context strict do_props (b, ths) (Facts {facts, props}) =
+fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
   let
     val (name, facts') =
       if Binding.is_empty b then ("", facts)
       else Name_Space.define context strict (b, Static ths) facts;
-    val props' =
-      if do_props
-      then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
-      else props;
+    val props' = props
+      |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths;
   in (name, make_facts facts' props') end;
 
-in
-
-fun add_global context = add context true false;
-fun add_local context = add context false;
-
-end;
-
 
 (* add dynamic entries *)
 

--- a/src/Pure/global_theory.ML	Tue Oct 09 15:31:45 2012 +0200
+++ b/src/Pure/global_theory.ML	Tue Oct 09 19:24:19 2012 +0200
@@ -134,7 +134,8 @@
       val name = Sign.full_name thy b;
       val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
       val thms'' = map (Thm.transfer thy') thms';
-      val thy'' = thy' |> Data.map (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
+      val thy'' = thy' |> Data.map
+        (Facts.add_static (Context.Theory thy') {strict = true, index = false} (b, thms'') #> snd);
     in (thms'', thy'') end;