src/Pure/facts.ML

   val dest_static: T list -> T -> (string * thm list) list
   val extern_static: Proof.context -> T list -> T -> (xstring * thm list) list
   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
 end;
 

   in make_facts facts' props' end;
 
 
 (* 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 *)
 
 fun add_dynamic context (b, f) (Facts {facts, props}) =