src/Pure/Isar/object_logic.ML

--- a/src/Pure/Isar/object_logic.ML	Thu Oct 04 16:21:31 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML	Thu Oct 04 16:59:28 2007 +0200
@@ -160,7 +160,8 @@
 
 fun atomize_prems ct =
   if Logic.has_meta_prems (Thm.term_of ct) then
-    Conv.forall_conv ~1 (Conv.prems_conv ~1 atomize) ct
+    Conv.forall_conv ~1 (K (Conv.prems_conv ~1 atomize))
+      (ProofContext.init (Thm.theory_of_cterm ct)) ct
   else Conv.all_conv ct;
 
 val atomize_prems_tac = CONVERSION atomize_prems;