1224 = SOME (SOME false)) |
1224 = SOME (SOME false)) |
1225 in fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) end |
1225 in fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) end |
1226 |
1226 |
1227 (** Preprocessor entry point **) |
1227 (** Preprocessor entry point **) |
1228 |
1228 |
|
1229 val max_skolem_depth = 4 |
|
1230 |
1229 fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs, |
1231 fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs, |
1230 boxes, skolemize, ...}) finitizes monos t = |
1232 boxes, ...}) finitizes monos t = |
1231 let |
1233 let |
1232 val skolem_depth = if skolemize then 4 else ~1 |
|
1233 val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) = |
1234 val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) = |
1234 t |> unfold_defs_in_term hol_ctxt |
1235 t |> unfold_defs_in_term hol_ctxt |
1235 |> close_form |
1236 |> close_form |
1236 |> skolemize_term_and_more hol_ctxt skolem_depth |
1237 |> skolemize_term_and_more hol_ctxt max_skolem_depth |
1237 |> specialize_consts_in_term hol_ctxt 0 |
1238 |> specialize_consts_in_term hol_ctxt 0 |
1238 |> axioms_for_term hol_ctxt |
1239 |> axioms_for_term hol_ctxt |
1239 val binarize = |
1240 val binarize = |
1240 is_standard_datatype thy stds nat_T andalso |
1241 is_standard_datatype thy stds nat_T andalso |
1241 case binary_ints of |
1242 case binary_ints of |