make SML/NJ happy, by adhoc type-constraints;
authorwenzelm
Wed Jul 21 17:57:16 2010 +0200 (2010-07-21)
changeset 37901ea7d4423cb5b
parent 37900 8b3498b9eb4b
child 37902 4e7864f3643d
child 37921 1e846be00ddf
make SML/NJ happy, by adhoc type-constraints;
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Wed Jul 21 17:55:07 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Wed Jul 21 17:57:16 2010 +0200
     1.3 @@ -414,7 +414,7 @@
     1.4  
     1.5  (* prove simplification equations *)
     1.6  
     1.7 -fun prove_eqs quiet_mode cs params intr_ts intrs elims ctxt ctxt'' =
     1.8 +fun prove_eqs quiet_mode cs params intr_ts intrs (elims: (thm * bstring list * int) list) ctxt ctxt'' =
     1.9    let
    1.10      val _ = clean_message quiet_mode "  Proving the simplification rules ...";
    1.11      
    1.12 @@ -422,7 +422,7 @@
    1.13        (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
    1.14         Logic.strip_assums_hyp r, Logic.strip_params r);
    1.15      val intr_ts' = map dest_intr intr_ts;
    1.16 -    fun prove_eq c elim =
    1.17 +    fun prove_eq c (elim: thm * 'a * 'b) =
    1.18        let
    1.19          val Ts = arg_types_of (length params) c;
    1.20          val (anames, ctxt') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt;