src/Pure/Isar/object_logic.ML

--- a/src/Pure/Isar/object_logic.ML	Mon Apr 07 15:37:34 2008 +0200
+++ b/src/Pure/Isar/object_logic.ML	Mon Apr 07 21:25:18 2008 +0200
@@ -206,7 +206,7 @@
 
 fun atomize_prems ct =
   if Logic.has_meta_prems (Thm.term_of ct) then
-    Conv.forall_conv ~1 (K (Conv.prems_conv ~1 atomize))
+    Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
       (ProofContext.init (Thm.theory_of_cterm ct)) ct
   else Conv.all_conv ct;