diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/variable.ML	Mon May 03 14:25:56 2010 +0200
@@ -235,7 +235,7 @@
 val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
 
 val declare_thm = Thm.fold_terms declare_internal;
-fun global_thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
+fun global_thm_context th = declare_thm th (ProofContext.init_global (Thm.theory_of_thm th));
 
 
 (* renaming term/type frees *)