diff -r 1fc86cec3bdf -r 5e8cef567042 src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Fri Oct 02 22:15:30 2009 +0200
+++ b/src/Tools/induct_tacs.ML	Fri Oct 02 23:15:36 2009 +0200
@@ -28,7 +28,7 @@
 
 fun gen_case_tac ctxt0 s opt_rule i st =
   let
-    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
+    val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
     val rule =
       (case opt_rule of
         SOME rule => rule