1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Oct 09 15:31:45 2012 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Oct 09 19:24:19 2012 +0200
     1.3 @@ -938,8 +938,8 @@
     1.4  local
     1.5  
     1.6  fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
     1.7 -  | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
     1.8 -      (Facts.add_local (Context.Proof ctxt) do_props (b, ths) #> snd);
     1.9 +  | update_thms flags (b, SOME ths) ctxt = ctxt |> map_facts
    1.10 +      (Facts.add_static (Context.Proof ctxt) flags (b, ths) #> snd);
    1.11  
    1.12  in
    1.13  
    1.14 @@ -952,12 +952,12 @@
    1.15      val (res, ctxt') = fold_map app facts ctxt;
    1.16      val thms = Global_Theory.name_thms false false name (flat res);
    1.17      val Mode {stmt, ...} = get_mode ctxt;
    1.18 -  in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
    1.19 +  in ((name, thms), ctxt' |> update_thms {strict = false, index = stmt} (b, SOME thms)) end);
    1.20  
    1.21 -fun put_thms do_props thms ctxt = ctxt
    1.22 +fun put_thms index thms ctxt = ctxt
    1.23    |> map_naming (K Name_Space.local_naming)
    1.24    |> Context_Position.set_visible false
    1.25 -  |> update_thms do_props (apfst Binding.name thms)
    1.26 +  |> update_thms {strict = false, index = index} (apfst Binding.name thms)
    1.27    |> Context_Position.restore_visible ctxt
    1.28    |> restore_naming ctxt;
    1.29  

     2.1 --- a/src/Pure/facts.ML	Tue Oct 09 15:31:45 2012 +0200
     2.2 +++ b/src/Pure/facts.ML	Tue Oct 09 19:24:19 2012 +0200
     2.3 @@ -32,8 +32,8 @@
     2.4    val props: T -> thm list
     2.5    val could_unify: T -> term -> thm list
     2.6    val merge: T * T -> T
     2.7 -  val add_global: Context.generic -> binding * thm list -> T -> string * T
     2.8 -  val add_local: Context.generic -> bool -> binding * thm list -> T -> string * T
     2.9 +  val add_static: Context.generic -> {strict: bool, index: bool} ->
    2.10 +    binding * thm list -> T -> string * T
    2.11    val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
    2.12    val del: string -> T -> T
    2.13    val hide: bool -> string -> T -> T
    2.14 @@ -188,26 +188,15 @@
    2.15  
    2.16  (* add static entries *)
    2.17  
    2.18 -local
    2.19 -
    2.20 -fun add context strict do_props (b, ths) (Facts {facts, props}) =
    2.21 +fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
    2.22    let
    2.23      val (name, facts') =
    2.24        if Binding.is_empty b then ("", facts)
    2.25        else Name_Space.define context strict (b, Static ths) facts;
    2.26 -    val props' =
    2.27 -      if do_props
    2.28 -      then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
    2.29 -      else props;
    2.30 +    val props' = props
    2.31 +      |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths;
    2.32    in (name, make_facts facts' props') end;
    2.33  
    2.34 -in
    2.35 -
    2.36 -fun add_global context = add context true false;
    2.37 -fun add_local context = add context false;
    2.38 -
    2.39 -end;
    2.40 -
    2.41  
    2.42  (* add dynamic entries *)
    2.43  

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