src/HOL/ex/Classpackage.thy
changeset 19933 16a5037f2d25
parent 19928 cb8472f4c5fd
child 19951 d58e2c564100
--- a/src/HOL/ex/Classpackage.thy	Tue Jun 20 16:46:30 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy	Wed Jun 21 10:26:39 2006 +0200
@@ -166,7 +166,7 @@
 proof (induct n)
   case 0 with neutl npow_def show ?case by simp
 next
-  case (Suc n) with prems assoc npow_def show ?case by simp
+  case (Suc n) with Suc.hyps assoc npow_def show ?case by simp
 qed
 
 lemma (in monoid) nat_pow_pow: