--- a/src/HOL/Tools/inductive.ML Wed Jul 21 17:55:07 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Jul 21 17:57:16 2010 +0200
@@ -414,7 +414,7 @@
(* 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 ...";
@@ -422,7 +422,7 @@
(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;