diff -r f8c5e218e4d8 -r 61ffcf4c02c7 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Tue Jul 03 17:17:15 2007 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Tue Jul 03 17:17:16 2007 +0200
@@ -189,7 +189,7 @@
 
 fun unfold_prems n defs th =
   if null defs then th
-  else Conv.fconv_rule (Conv.goals_conv (fn i => i <= n) (MetaSimplifier.rewrite true defs)) th;
+  else Conv.fconv_rule (Conv.prems_conv n (K (MetaSimplifier.rewrite true defs))) th;
 
 fun unfold_prems_concls defs th =
   if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th