diff -r 0a567f923b42 -r ee9d53fbb56b ProgTutorial/Package/simple_inductive_package.ML
--- a/ProgTutorial/Package/simple_inductive_package.ML	Tue Jul 28 12:11:33 2009 +0200
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Thu Jul 30 11:38:52 2009 +0200
@@ -129,7 +129,7 @@
  SUBPROOF (fn {params, prems, context = ctxt', ...} =>
   let
     val (prems1, prems2) = chop (length prems - length rules) prems;
-    val (params1, params2) = chop (length params - length preds) params;
+    val (params1, params2) = chop (length params - length preds) (map snd params);
   in
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 
     THEN