# HG changeset patch
# User haftmann
# Date 1417013177 -3600
# Node ID 97b089c4aa4610770f5685fba21099e709d4e144
# Parent  a78612c67ec021e985fd6aeb09fcb87f13e1d5ee
tuned

diff -r a78612c67ec0 -r 97b089c4aa46 src/HOL/Tools/inductive.ML
--- 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 *)