in

   in

     Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)

     Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)

                             |> map Logic.mk_equals,

                             |> map Logic.mk_equals,

                         Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),

                         Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),

                                          list_comb (Const x2, bounds2 @ args2)))

                                          list_comb (Const x2, bounds2 @ args2)))

   end

   end

 (* hol_context -> styp list -> term list *)

 (* hol_context -> styp list -> term list *)

 fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =

 fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =

   let

   let

                                   skolemize, uncurry, ...}) t =

                                   skolemize, uncurry, ...}) t =

   let

   let

     val skolem_depth = if skolemize then 4 else ~1

     val skolem_depth = if skolemize then 4 else ~1

     val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),

     val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),

          core_t) = t |> unfold_defs_in_term hol_ctxt

          core_t) = t |> unfold_defs_in_term hol_ctxt

                      |> skolemize_term_and_more hol_ctxt skolem_depth

                      |> skolemize_term_and_more hol_ctxt skolem_depth

                      |> specialize_consts_in_term hol_ctxt 0

                      |> specialize_consts_in_term hol_ctxt 0

                      |> `(axioms_for_term hol_ctxt)

                      |> `(axioms_for_term hol_ctxt)

     val binarize =

     val binarize =

       case binary_ints of

       case binary_ints of

       #> destroy_universal_equalities

       #> destroy_universal_equalities

       #> destroy_existential_equalities thy

       #> destroy_existential_equalities thy

       #> simplify_constrs_and_sels thy

       #> simplify_constrs_and_sels thy

       #> distribute_quantifiers

       #> distribute_quantifiers

       #> push_quantifiers_inward thy

       #> push_quantifiers_inward thy

       #> Term.map_abs_vars shortest_name

       #> Term.map_abs_vars shortest_name

   in

   in

     (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),

     (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),

       (got_all_mono_user_axioms, no_poly_user_axioms)),

       (got_all_mono_user_axioms, no_poly_user_axioms)),

      do_rest false true core_t)

      do_rest false true core_t)