src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 46107 e740ffcd0ef4
parent 46102 b669437de253
child 46113 dd112cd72c48
     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