src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 55888 cac1add157e8
parent 55628 8103021024c1
child 55889 6bfbec3dff62
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Mar 03 16:44:46 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -129,7 +129,7 @@
     1.4  fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
     1.5      could_exist_alpha_subtype alpha_T T
     1.6    | could_exist_alpha_sub_mtype ctxt alpha_T T =
     1.7 -    (T = alpha_T orelse is_datatype ctxt [(NONE, true)] T)
     1.8 +    (T = alpha_T orelse is_datatype ctxt T)
     1.9  
    1.10  fun exists_alpha_sub_mtype MAlpha = true
    1.11    | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
    1.12 @@ -737,13 +737,11 @@
    1.13                                             frame2)
    1.14    end
    1.15  
    1.16 -fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
    1.17 -                             max_fresh, ...}) =
    1.18 +fun consider_term (mdata as {hol_ctxt = {ctxt, ...}, alpha_T, max_fresh, ...}) =
    1.19    let
    1.20      fun is_enough_eta_expanded t =
    1.21        case strip_comb t of
    1.22 -        (Const x, ts) => the_default 0 (arity_of_built_in_const thy stds x)
    1.23 -        <= length ts
    1.24 +        (Const x, ts) => the_default 0 (arity_of_built_in_const x) <= length ts
    1.25        | _ => true
    1.26      val mtype_for = fresh_mtype_for_type mdata false
    1.27      fun mtype_for_set x T = MFun (mtype_for (pseudo_domain_type T), V x, bool_M)
    1.28 @@ -894,9 +892,9 @@
    1.29                  do_fragile_set_operation T accum
    1.30                else if is_sel s then
    1.31                  (mtype_for_sel mdata x, accum)
    1.32 -              else if is_constr ctxt stds x then
    1.33 +              else if is_constr ctxt x then
    1.34                  (mtype_for_constr mdata x, accum)
    1.35 -              else if is_built_in_const thy stds x then
    1.36 +              else if is_built_in_const x then
    1.37                  (fresh_mtype_for_type mdata true T, accum)
    1.38                else
    1.39                  let val M = mtype_for T in
    1.40 @@ -1074,20 +1072,20 @@
    1.41    [@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
    1.42  val bounteous_consts = [@{const_name bisim}]
    1.43  
    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 -        exists (member (op =) bounteous_consts o fst))
    1.49 +fun is_harmless_axiom t =
    1.50 +  Term.add_consts t []
    1.51 +  |> filter_out is_built_in_const
    1.52 +  |> (forall (member (op =) harmless_consts o original_name o fst) orf
    1.53 +      exists (member (op =) bounteous_consts o fst))
    1.54  
    1.55  fun consider_nondefinitional_axiom mdata t =
    1.56 -  if is_harmless_axiom mdata t then I
    1.57 +  if is_harmless_axiom t then I
    1.58    else consider_general_formula mdata Plus t
    1.59  
    1.60  fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...} : mdata) t =
    1.61    if not (is_constr_pattern_formula ctxt t) then
    1.62      consider_nondefinitional_axiom mdata t
    1.63 -  else if is_harmless_axiom mdata t then
    1.64 +  else if is_harmless_axiom t then
    1.65      I
    1.66    else
    1.67      let