# HG changeset patch
# User krauss
# Date 1292022852 -3600
# Node ID 97bf008b9cfeb3c02f2d334161ca60e30bd10de9
# Parent  3f22550e442fb14b478b0a1cd7b99f32716fcc31
made smlnj happy

diff -r 3f22550e442f -r 97bf008b9cfe src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Dec 10 16:10:57 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Dec 11 00:14:12 2010 +0100
@@ -459,8 +459,8 @@
      NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
    | SOME clauses => (comps, clauses))
 
-val add_mtype_is_concrete = add_notin_mtype_fv Minus
-val add_mtype_is_complete = add_notin_mtype_fv Plus
+fun add_mtype_is_concrete x y z = add_notin_mtype_fv Minus x y z
+fun add_mtype_is_complete x y z = add_notin_mtype_fv Plus x y z
 
 val bool_table =
   [(Gen, (false, false)),
@@ -583,7 +583,7 @@
 fun string_for_free relevant_frees ((s, _), M) =
   if member (op =) relevant_frees s then SOME (s ^ " : " ^ string_for_mtype M)
   else NONE
-fun string_for_mcontext ctxt t {bound_Ms, frame, frees, ...} =
+fun string_for_mcontext ctxt t ({bound_Ms, frame, frees, ...} : mcontext) =
   (map_filter (string_for_free (Term.add_free_names t [])) frees @
    map (string_for_bound ctxt bound_Ms) frame)
   |> commas |> enclose "[" "]"
@@ -678,13 +678,13 @@
                    add_connective_var conn mk_quasi_clauses res_aa aa1 aa2)
                res_frame frame1 frame2)
 
-fun kill_unused_in_frame is_in (accum as ({frame, ...}, _)) =
+fun kill_unused_in_frame is_in (accum as ({frame, ...} : mcontext, _)) =
   let val (used_frame, unused_frame) = List.partition is_in frame in
     accum |>> set_frame used_frame
           ||> add_comp_frame (A Gen) Eq unused_frame
   end
 
-fun split_frame is_in_fun (gamma as {frame, ...}, cset) =
+fun split_frame is_in_fun (gamma as {frame, ...} : mcontext, cset) =
   let
     fun bubble fun_frame arg_frame [] cset =
         ((rev fun_frame, rev arg_frame), cset)
@@ -1072,7 +1072,7 @@
   [@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
 val bounteous_consts = [@{const_name bisim}]
 
-fun is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
+fun is_harmless_axiom ({hol_ctxt = {thy, stds, ...}, ...} : mdata) t =
     Term.add_consts t []
     |> filter_out (is_built_in_const thy stds)
     |> (forall (member (op =) harmless_consts o original_name o fst) orf
@@ -1082,7 +1082,7 @@
   if is_harmless_axiom mdata t then I
   else consider_general_formula mdata Plus t
 
-fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t =
+fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...} : mdata) t =
   if not (is_constr_pattern_formula ctxt t) then
     consider_nondefinitional_axiom mdata t
   else if is_harmless_axiom mdata t then