src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 35832 1dac16f00cd2
parent 35812 394fe2b064cd
child 36385 ff5f88702590
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Mar 18 13:59:20 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Mar 18 14:52:11 2010 +0100
     1.3 @@ -451,7 +451,7 @@
     1.4                   [M1, M2], [])
     1.5  
     1.6  (* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *)
     1.7 -fun add_mtype_comp cmp M1 M2 (lits, comps, sexps) =
     1.8 +fun add_mtype_comp cmp M1 M2 ((lits, comps, sexps) : constraint_set) =
     1.9      (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^
    1.10                " " ^ string_for_mtype M2);
    1.11       case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
    1.12 @@ -500,7 +500,7 @@
    1.13      raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
    1.14  
    1.15  (* sign -> mtyp -> constraint_set -> constraint_set *)
    1.16 -fun add_notin_mtype_fv sn M (lits, comps, sexps) =
    1.17 +fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) =
    1.18      (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^
    1.19                (case sn of Minus => "concrete" | Plus => "complete") ^ ".");
    1.20       case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of