src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 41052 3db267a01c1d
parent 41001 11715564e2ad
child 41791 01d722707a36
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 07 11:56:53 2010 +0100
     1.3 @@ -9,8 +9,7 @@
     1.4  sig
     1.5    type hol_context = Nitpick_HOL.hol_context
     1.6    val preprocess_formulas :
     1.7 -    hol_context -> (typ option * bool option) list
     1.8 -    -> (typ option * bool option) list -> term list -> term
     1.9 +    hol_context -> term list -> term
    1.10      -> term list * term list * bool * bool * bool
    1.11  end;
    1.12  
    1.13 @@ -1245,32 +1244,13 @@
    1.14               | _ => t
    1.15    in aux "" [] [] end
    1.16  
    1.17 -(** Inference of finite functions **)
    1.18 -
    1.19 -fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos
    1.20 -                               (nondef_ts, def_ts) =
    1.21 -  if forall (curry (op =) (SOME false) o snd) finitizes then
    1.22 -    (nondef_ts, def_ts)
    1.23 -  else
    1.24 -    let
    1.25 -      val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
    1.26 -               |> filter_out (fn Type (@{type_name fun_box}, _) => true
    1.27 -                               | @{typ signed_bit} => true
    1.28 -                               | @{typ unsigned_bit} => true
    1.29 -                               | T => is_small_finite_type hol_ctxt T orelse
    1.30 -                                      triple_lookup (type_match thy) monos T
    1.31 -                                      = SOME (SOME false))
    1.32 -    in
    1.33 -      fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts)
    1.34 -    end
    1.35 -
    1.36  (** Preprocessor entry point **)
    1.37  
    1.38  val max_skolem_depth = 3
    1.39  
    1.40  fun preprocess_formulas
    1.41          (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
    1.42 -                      ...}) finitizes monos assm_ts neg_t =
    1.43 +                      ...}) assm_ts neg_t =
    1.44    let
    1.45      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
    1.46        neg_t |> unfold_defs_in_term hol_ctxt
    1.47 @@ -1307,9 +1287,6 @@
    1.48        #> Term.map_abs_vars shortest_name
    1.49      val nondef_ts = map (do_rest false) nondef_ts
    1.50      val def_ts = map (do_rest true) def_ts
    1.51 -    val (nondef_ts, def_ts) =
    1.52 -      finitize_all_types_of_funs hol_ctxt binarize finitizes monos
    1.53 -                                 (nondef_ts, def_ts)
    1.54    in
    1.55      (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
    1.56    end