--- a/src/Pure/facts.ML Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/facts.ML Sun Apr 17 19:54:04 2011 +0200
@@ -32,9 +32,10 @@
val props: T -> thm list
val could_unify: T -> term -> thm list
val merge: T * T -> T
- val add_global: Name_Space.naming -> binding * thm list -> T -> string * T
- val add_local: bool -> Name_Space.naming -> binding * thm list -> T -> string * T
- val add_dynamic: Name_Space.naming -> binding * (Context.generic -> thm list) -> T -> string * T
+ val add_global: Proof.context -> Name_Space.naming -> binding * thm list -> T -> string * T
+ val add_local: Proof.context -> bool -> Name_Space.naming -> binding * thm list -> T -> string * T
+ val add_dynamic: Proof.context -> Name_Space.naming ->
+ binding * (Context.generic -> thm list) -> T -> string * T
val del: string -> T -> T
val hide: bool -> string -> T -> T
end;
@@ -190,11 +191,11 @@
local
-fun add strict do_props naming (b, ths) (Facts {facts, props}) =
+fun add ctxt strict do_props naming (b, ths) (Facts {facts, props}) =
let
val (name, facts') =
if Binding.is_empty b then ("", facts)
- else Name_Space.define strict naming (b, Static ths) facts;
+ else Name_Space.define ctxt strict naming (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
@@ -203,16 +204,16 @@
in
-val add_global = add true false;
-val add_local = add false;
+fun add_global ctxt = add ctxt true false;
+fun add_local ctxt = add ctxt false;
end;
(* add dynamic entries *)
-fun add_dynamic naming (b, f) (Facts {facts, props}) =
- let val (name, facts') = Name_Space.define true naming (b, Dynamic f) facts;
+fun add_dynamic ctxt naming (b, f) (Facts {facts, props}) =
+ let val (name, facts') = Name_Space.define ctxt true naming (b, Dynamic f) facts;
in (name, make_facts facts' props) end;