--- a/src/HOL/Tools/inductive.ML Wed Nov 26 20:05:34 2014 +0100
+++ b/src/HOL/Tools/inductive.ML Wed Nov 26 15:46:17 2014 +0100
@@ -510,7 +510,7 @@
(if null ts andalso null us then resolve_tac [intr] 1
else
EVERY (replicate (length ts + length us - 1) (eresolve_tac @{thms conjE} 1)) THEN
- Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
+ Subgoal.FOCUS_PREMS (fn {context = ctxt'', prems, ...} =>
let
val (eqs, prems') = chop (length us) prems;
val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
@@ -1003,11 +1003,8 @@
(* external interfaces *)
fun gen_add_inductive_i mk_def
- (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono})
- cnames_syn pnames spec monos lthy =
+ flags cnames_syn pnames spec monos lthy =
let
- val thy = Proof_Context.theory_of lthy;
-
(* abbrevs *)