# HG changeset patch
# User wenzelm
# Date 1279727836 -7200
# Node ID ea7d4423cb5be4b43c40da677530b175de9cfefa
# Parent  8b3498b9eb4b337e9e1214f90f44e96cfee7df2b
make SML/NJ happy, by adhoc type-constraints;

diff -r 8b3498b9eb4b -r ea7d4423cb5b src/HOL/Tools/inductive.ML
--- 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;