fixed bisimilarity axiom -- avoid "insert" with wrong type
authorblanchet
Tue Jan 03 23:41:59 2012 +0100 (2012-01-03)
changeset 46107e740ffcd0ef4
parent 46106 73e2c70980df
child 46108 1c314d838676
fixed bisimilarity axiom -- avoid "insert" with wrong type
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 23:09:27 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 23:41:59 2012 +0100
     1.3 @@ -2004,8 +2004,7 @@
     1.4                                                (map case_func xs), x_var)),
     1.5          bisim_const T $ n_var $ x_var $ y_var),
     1.6       HOLogic.eq_const pred_T $ (bisim_const T $ bisim_max $ x_var)
     1.7 -     $ (Const (@{const_name insert}, T --> pred_T --> pred_T)
     1.8 -        $ x_var $ Const (@{const_name bot_class.bot}, pred_T))]
     1.9 +     $ Abs (Name.uu, T, HOLogic.mk_eq (x_var, Bound 0))]
    1.10      |> map HOLogic.mk_Trueprop
    1.11    end
    1.12