--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 03 23:09:27 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 03 23:41:59 2012 +0100
@@ -2004,8 +2004,7 @@
(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)
- $ (Const (@{const_name insert}, T --> pred_T --> pred_T)
- $ x_var $ Const (@{const_name bot_class.bot}, pred_T))]
+ $ Abs (Name.uu, T, HOLogic.mk_eq (x_var, Bound 0))]
|> map HOLogic.mk_Trueprop
end