--- a/prio/PrioG.thy	Fri Feb 10 11:30:47 2012 +0000
+++ b/prio/PrioG.thy	Fri Feb 10 21:01:03 2012 +0000
@@ -2072,14 +2072,17 @@
 qed
 
 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
-proof(unfold cp_def wq_def, induct s)
-  case (Cons e s')
-  show ?case
-    by (auto simp:Let_def)
-next
-  case Nil
-  show ?case by (auto simp:Let_def)
-qed
+unfolding cp_def wq_def
+apply(induct s rule: schs.induct)
+apply(simp add: Let_def cpreced_initial)
+apply(simp add: Let_def)
+apply(simp add: Let_def)
+apply(simp add: Let_def)
+apply(subst (2) schs.simps)
+apply(simp add: Let_def)
+apply(subst (2) schs.simps)
+apply(simp add: Let_def)
+done
 
 
 lemma runing_unique: