--- a/src/ZF/Tools/induct_tacs.ML Mon Mar 23 10:16:20 2015 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Mon Mar 23 13:30:59 2015 +0100
@@ -101,11 +101,11 @@
[] => error "induction is not available for this datatype"
| major::_ => FOLogic.dest_Trueprop major)
in
- Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] rule i
+ Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] [] rule i
end
handle Find_tname msg =>
if exh then (*try boolean case analysis instead*)
- case_tac ctxt var i
+ case_tac ctxt var [] i
else error msg) i state;
val exhaust_tac = exhaust_induct_tac true;