# 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