src/Tools/induct_tacs.ML
changeset 32863 5e8cef567042
parent 30541 9f168bdc468a
child 33368 b1cf34f1855c
equal deleted inserted replaced
32862:1fc86cec3bdf 32863:5e8cef567042
    26       error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
    26       error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
    27   in (u, U) end;
    27   in (u, U) end;
    28 
    28 
    29 fun gen_case_tac ctxt0 s opt_rule i st =
    29 fun gen_case_tac ctxt0 s opt_rule i st =
    30   let
    30   let
    31     val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    31     val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
    32     val rule =
    32     val rule =
    33       (case opt_rule of
    33       (case opt_rule of
    34         SOME rule => rule
    34         SOME rule => rule
    35       | NONE =>
    35       | NONE =>
    36           (case Induct.find_casesT ctxt
    36           (case Induct.find_casesT ctxt