src/Pure/facts.ML

--- 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;