changeset 32863 | 5e8cef567042 |
parent 30541 | 9f168bdc468a |
child 33368 | b1cf34f1855c |
--- 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