# HG changeset patch
# User blanchet
# Date 1268920331 -3600
# Node ID 1dac16f00cd2ae85e9200be2d1b3984481ebd318
# Parent  e31ec41a551b9e401b67d003e8af19555b287344
added type constraints to make SML/NJ happy

diff -r e31ec41a551b -r 1dac16f00cd2 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Mar 18 13:59:20 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Mar 18 14:52:11 2010 +0100
@@ -451,7 +451,7 @@
                  [M1, M2], [])
 
 (* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *)
-fun add_mtype_comp cmp M1 M2 (lits, comps, sexps) =
+fun add_mtype_comp cmp M1 M2 ((lits, comps, sexps) : constraint_set) =
     (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^
               " " ^ string_for_mtype M2);
      case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
@@ -500,7 +500,7 @@
     raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
 
 (* sign -> mtyp -> constraint_set -> constraint_set *)
-fun add_notin_mtype_fv sn M (lits, comps, sexps) =
+fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) =
     (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^
               (case sn of Minus => "concrete" | Plus => "complete") ^ ".");
      case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of