src/Tools/induct_tacs.ML
changeset 32863 5e8cef567042
parent 30541 9f168bdc468a
child 33368 b1cf34f1855c
     1.1 --- a/src/Tools/induct_tacs.ML	Fri Oct 02 22:15:30 2009 +0200
     1.2 +++ b/src/Tools/induct_tacs.ML	Fri Oct 02 23:15:36 2009 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  fun gen_case_tac ctxt0 s opt_rule i st =
     1.6    let
     1.7 -    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
     1.8 +    val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
     1.9      val rule =
    1.10        (case opt_rule of
    1.11          SOME rule => rule