src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 39359 6f49c7fbb1b1
parent 39345 062c10ff848c
child 39360 cdf2c3341422
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Sep 14 12:52:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Sep 14 13:24:18 2010 +0200
     1.3 @@ -549,13 +549,12 @@
     1.4     consts = consts}
     1.5    handle List.Empty => initial_gamma (* FIXME: needed? *)
     1.6  
     1.7 -fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs, ...},
     1.8 -                             alpha_T, max_fresh, ...}) =
     1.9 +fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
    1.10 +                             max_fresh, ...}) =
    1.11    let
    1.12      fun is_enough_eta_expanded t =
    1.13        case strip_comb t of
    1.14 -        (Const x, ts) =>
    1.15 -        the_default 0 (arity_of_built_in_const thy stds fast_descrs x)
    1.16 +        (Const x, ts) => the_default 0 (arity_of_built_in_const thy stds x)
    1.17          <= length ts
    1.18        | _ => true
    1.19      val mtype_for = fresh_mtype_for_type mdata false
    1.20 @@ -725,7 +724,7 @@
    1.21                    (mtype_for_sel mdata x, accum)
    1.22                  else if is_constr ctxt stds x then
    1.23                    (mtype_for_constr mdata x, accum)
    1.24 -                else if is_built_in_const thy stds fast_descrs x then
    1.25 +                else if is_built_in_const thy stds x then
    1.26                    (fresh_mtype_for_type mdata true T, accum)
    1.27                  else
    1.28                    let val M = mtype_for T in
    1.29 @@ -908,9 +907,9 @@
    1.30  val bounteous_consts = [@{const_name bisim}]
    1.31  
    1.32  fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
    1.33 -  | is_harmless_axiom {hol_ctxt = {thy, stds, fast_descrs, ...}, ...} t =
    1.34 +  | is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
    1.35      Term.add_consts t []
    1.36 -    |> filter_out (is_built_in_const thy stds fast_descrs)
    1.37 +    |> filter_out (is_built_in_const thy stds)
    1.38      |> (forall (member (op =) harmless_consts o original_name o fst) orf
    1.39          exists (member (op =) bounteous_consts o fst))
    1.40  
    1.41 @@ -1022,8 +1021,7 @@
    1.42  fun fin_fun_constr T1 T2 =
    1.43    (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
    1.44  
    1.45 -fun finitize_funs (hol_ctxt as {thy, ctxt, stds, fast_descrs, constr_cache,
    1.46 -                                ...})
    1.47 +fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...})
    1.48                    binarize finitizes alpha_T tsp =
    1.49    case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
    1.50      SOME (lits, msp, constr_mtypes) =>
    1.51 @@ -1074,7 +1072,7 @@
    1.52                        | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\
    1.53                                           \term_from_mterm", [T, T'], [])
    1.54                    in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end
    1.55 -                else if is_built_in_const thy stds fast_descrs x then
    1.56 +                else if is_built_in_const thy stds x then
    1.57                    coerce_term hol_ctxt new_Ts T' T t
    1.58                  else if is_constr ctxt stds x then
    1.59                    Const (finitize_constr x)