# HG changeset patch
# User blanchet
# Date 1325630519 -3600
# Node ID e740ffcd0ef405595203cbe446210507e0e4a113
# Parent  73e2c70980dfbb75866cfdac02822f5e782f86f3
fixed bisimilarity axiom -- avoid "insert" with wrong type

diff -r 73e2c70980df -r e740ffcd0ef4 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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