src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41109 97bf008b9cfe
parent 41054 e58d1cdda832
child 41471 54a58904a598
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Dec 10 16:10:57 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Dec 11 00:14:12 2010 +0100
     1.3 @@ -459,8 +459,8 @@
     1.4       NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
     1.5     | SOME clauses => (comps, clauses))
     1.6  
     1.7 -val add_mtype_is_concrete = add_notin_mtype_fv Minus
     1.8 -val add_mtype_is_complete = add_notin_mtype_fv Plus
     1.9 +fun add_mtype_is_concrete x y z = add_notin_mtype_fv Minus x y z
    1.10 +fun add_mtype_is_complete x y z = add_notin_mtype_fv Plus x y z
    1.11  
    1.12  val bool_table =
    1.13    [(Gen, (false, false)),
    1.14 @@ -583,7 +583,7 @@
    1.15  fun string_for_free relevant_frees ((s, _), M) =
    1.16    if member (op =) relevant_frees s then SOME (s ^ " : " ^ string_for_mtype M)
    1.17    else NONE
    1.18 -fun string_for_mcontext ctxt t {bound_Ms, frame, frees, ...} =
    1.19 +fun string_for_mcontext ctxt t ({bound_Ms, frame, frees, ...} : mcontext) =
    1.20    (map_filter (string_for_free (Term.add_free_names t [])) frees @
    1.21     map (string_for_bound ctxt bound_Ms) frame)
    1.22    |> commas |> enclose "[" "]"
    1.23 @@ -678,13 +678,13 @@
    1.24                     add_connective_var conn mk_quasi_clauses res_aa aa1 aa2)
    1.25                 res_frame frame1 frame2)
    1.26  
    1.27 -fun kill_unused_in_frame is_in (accum as ({frame, ...}, _)) =
    1.28 +fun kill_unused_in_frame is_in (accum as ({frame, ...} : mcontext, _)) =
    1.29    let val (used_frame, unused_frame) = List.partition is_in frame in
    1.30      accum |>> set_frame used_frame
    1.31            ||> add_comp_frame (A Gen) Eq unused_frame
    1.32    end
    1.33  
    1.34 -fun split_frame is_in_fun (gamma as {frame, ...}, cset) =
    1.35 +fun split_frame is_in_fun (gamma as {frame, ...} : mcontext, cset) =
    1.36    let
    1.37      fun bubble fun_frame arg_frame [] cset =
    1.38          ((rev fun_frame, rev arg_frame), cset)
    1.39 @@ -1072,7 +1072,7 @@
    1.40    [@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
    1.41  val bounteous_consts = [@{const_name bisim}]
    1.42  
    1.43 -fun is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
    1.44 +fun is_harmless_axiom ({hol_ctxt = {thy, stds, ...}, ...} : mdata) t =
    1.45      Term.add_consts t []
    1.46      |> filter_out (is_built_in_const thy stds)
    1.47      |> (forall (member (op =) harmless_consts o original_name o fst) orf
    1.48 @@ -1082,7 +1082,7 @@
    1.49    if is_harmless_axiom mdata t then I
    1.50    else consider_general_formula mdata Plus t
    1.51  
    1.52 -fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t =
    1.53 +fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...} : mdata) t =
    1.54    if not (is_constr_pattern_formula ctxt t) then
    1.55      consider_nondefinitional_axiom mdata t
    1.56    else if is_harmless_axiom mdata t then