diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/facts.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -23,12 +23,12 @@
   val space_of: T -> Name_Space.T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
-  val extern: T -> string -> xstring
+  val extern: Proof.context -> T -> string -> xstring
   val lookup: Context.generic -> T -> string -> (bool * thm list) option
   val defined: T -> string -> bool
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   val dest_static: T list -> T -> (string * thm list) list
-  val extern_static: T list -> T -> (xstring * 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
@@ -141,7 +141,7 @@
 val is_concealed = Name_Space.is_concealed o space_of;
 
 val intern = Name_Space.intern o space_of;
-val extern = Name_Space.extern o space_of;
+fun extern ctxt = Name_Space.extern ctxt o space_of;
 
 val defined = Symtab.defined o table_of;
 
@@ -165,8 +165,8 @@
 fun dest_static prev_facts facts =
   sort_wrt #1 (diff_table prev_facts facts);
 
-fun extern_static prev_facts facts =
-  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern facts)));
+fun extern_static ctxt prev_facts facts =
+  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern ctxt facts)));
 
 
 (* indexed props *)