src/Pure/Isar/object_logic.ML

--- a/src/Pure/Isar/object_logic.ML	Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/object_logic.ML	Sat Apr 16 15:47:52 2011 +0200
@@ -188,7 +188,7 @@
 fun atomize_prems ct =
   if Logic.has_meta_prems (Thm.term_of ct) then
     Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
-      (ProofContext.init_global (Thm.theory_of_cterm ct)) ct
+      (Proof_Context.init_global (Thm.theory_of_cterm ct)) ct
   else Conv.all_conv ct;
 
 val atomize_prems_tac = CONVERSION atomize_prems;