fixed bisimilarity axiom -- avoid "insert" with wrong type
authorblanchet
Tue, 03 Jan 2012 23:41:59 +0100
changeset 46107 e740ffcd0ef4
parent 46106 73e2c70980df
child 46108 1c314d838676
fixed bisimilarity axiom -- avoid "insert" with wrong type
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