--- a/ProgTutorial/Package/Ind_Code.thy	Tue Jul 28 12:11:33 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Thu Jul 30 11:38:52 2009 +0200
@@ -633,7 +633,7 @@
 ML{*fun chop_test_tac preds rules =
   SUBPROOF_test (fn {params, prems, context, ...} =>
   let
-    val (params1, params2) = chop (length params - length preds) params
+    val (params1, params2) = chop (length params - length preds) (map snd params)
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
     chop_print params1 params2 prems1 prems2 context; no_tac
@@ -698,7 +698,7 @@
 ML %linenosgray{*fun apply_prem_tac i preds rules =
   SUBPROOF_test (fn {params, prems, context, ...} =>
   let
-    val (params1, params2) = chop (length params - length preds) params
+    val (params1, params2) = chop (length params - length preds) (map snd params)
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
@@ -773,7 +773,7 @@
 ML{*fun prove_intro_tac i preds rules =
   SUBPROOF (fn {params, prems, ...} =>
   let
-    val (params1, params2) = chop (length params - length preds) params
+    val (params1, params2) = chop (length params - length preds) (map snd params)
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
@@ -868,7 +868,7 @@
 ML %linenosgray{*fun prove_intro_tac i preds rules =
   SUBPROOF (fn {params, prems, context, ...} =>
   let
-    val (params1, params2) = chop (length params - length preds) params
+    val (params1, params2) = chop (length params - length preds) (map snd params)
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1