# HG changeset patch
# User blanchet
# Date 1626265495 -7200
# Node ID 906ecb04914141ea2a676dbcb51add177c3ecd29
# Parent  2d8a0f8e30ec76fc6df426cf9f3def83592b2e21
rephrase Nitpick constraint in more first-order format that's also more friendly to the 'box' option

diff -r 2d8a0f8e30ec -r 906ecb049141 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jul 14 10:02:43 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jul 14 14:24:55 2021 +0200
@@ -2058,8 +2058,9 @@
        (HOLogic.mk_disj (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T,
             s_betapply [] (optimized_case_def hol_ctxt [] T bool_T (map case_func xs), x_var)),
         bisim_const T $ n_var $ x_var $ y_var),
-     HOLogic.eq_const pred_T $ (bisim_const T $ bisim_max $ x_var)
-     $ Abs (Name.uu, T, HOLogic.mk_eq (x_var, Bound 0))]
+     HOLogic.mk_imp
+       (bisim_const T $ bisim_max $ x_var $ y_var,
+        HOLogic.mk_eq (x_var, y_var))]
     |> map HOLogic.mk_Trueprop
   end