1.1 --- a/src/Pure/facts.ML	Sun Mar 18 12:51:44 2012 +0100
     1.2 +++ b/src/Pure/facts.ML	Sun Mar 18 13:04:22 2012 +0100
     1.3 @@ -32,10 +32,9 @@
     1.4    val props: T -> thm list
     1.5    val could_unify: T -> term -> thm list
     1.6    val merge: T * T -> T
     1.7 -  val add_global: Proof.context -> Name_Space.naming -> binding * thm list -> T -> string * T
     1.8 -  val add_local: Proof.context -> bool -> Name_Space.naming -> binding * thm list -> T -> string * T
     1.9 -  val add_dynamic: Proof.context -> Name_Space.naming ->
    1.10 -    binding * (Context.generic -> thm list) -> T -> string * T
    1.11 +  val add_global: Context.generic -> binding * thm list -> T -> string * T
    1.12 +  val add_local: Context.generic -> bool -> binding * thm list -> T -> string * T
    1.13 +  val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
    1.14    val del: string -> T -> T
    1.15    val hide: bool -> string -> T -> T
    1.16  end;
    1.17 @@ -191,11 +190,11 @@
    1.18  
    1.19  local
    1.20  
    1.21 -fun add ctxt strict do_props naming (b, ths) (Facts {facts, props}) =
    1.22 +fun add context strict do_props (b, ths) (Facts {facts, props}) =
    1.23    let
    1.24      val (name, facts') =
    1.25        if Binding.is_empty b then ("", facts)
    1.26 -      else Name_Space.define ctxt strict naming (b, Static ths) facts;
    1.27 +      else Name_Space.define context strict (b, Static ths) facts;
    1.28      val props' =
    1.29        if do_props
    1.30        then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
    1.31 @@ -204,16 +203,16 @@
    1.32  
    1.33  in
    1.34  
    1.35 -fun add_global ctxt = add ctxt true false;
    1.36 -fun add_local ctxt = add ctxt false;
    1.37 +fun add_global context = add context true false;
    1.38 +fun add_local context = add context false;
    1.39  
    1.40  end;
    1.41  
    1.42  
    1.43  (* add dynamic entries *)
    1.44  
    1.45 -fun add_dynamic ctxt naming (b, f) (Facts {facts, props}) =
    1.46 -  let val (name, facts') = Name_Space.define ctxt true naming (b, Dynamic f) facts;
    1.47 +fun add_dynamic context (b, f) (Facts {facts, props}) =
    1.48 +  let val (name, facts') = Name_Space.define context true (b, Dynamic f) facts;
    1.49    in (name, make_facts facts' props) end;
    1.50  
    1.51