--- a/src/Tools/induct.ML Wed Apr 08 19:39:08 2015 +0200
+++ b/src/Tools/induct.ML Wed Apr 08 19:58:52 2015 +0200
@@ -731,7 +731,7 @@
type case_data = (((string * string list) * string list) list * int);
fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
- SUBGOAL_CASES (fn (_, i, st) =>
+ SUBGOAL_CASES (fn (_, i) =>
let
val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
@@ -820,7 +820,7 @@
in
-fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) =>
+fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i) =>
let
fun inst_rule r =
if null inst then `Rule_Cases.get r