src/HOL/Tools/inductive.ML

 
    in map prove_elim cs end;
 
 (* prove simplification equations *)
 
-fun prove_eqs quiet_mode cs params intr_ts intrs elims ctxt ctxt'' =
+fun prove_eqs quiet_mode cs params intr_ts intrs (elims: (thm * bstring list * int) list) ctxt ctxt'' =
   let
     val _ = clean_message quiet_mode "  Proving the simplification rules ...";
     
     fun dest_intr r =
       (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
        Logic.strip_assums_hyp r, Logic.strip_params r);
     val intr_ts' = map dest_intr intr_ts;
-    fun prove_eq c elim =
+    fun prove_eq c (elim: thm * 'a * 'b) =
       let
         val Ts = arg_types_of (length params) c;
         val (anames, ctxt') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt;
         val frees = map Free (anames ~~ Ts);
         val c_intrs = filter (equal c o #1 o #1 o #1) (intr_ts' ~~ intrs);