src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 46113 dd112cd72c48
parent 46107 e740ffcd0ef4
child 46115 ecab67f5a5c2
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 04 12:09:53 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 04 12:09:53 2012 +0100
     1.3 @@ -1982,8 +1982,7 @@
     1.4                            $ (suc_const iter_T $ Bound 0) $ n_var)
     1.5      val x_var = Var (("x", 0), T)
     1.6      val y_var = Var (("y", 0), T)
     1.7 -    fun bisim_const T =
     1.8 -      Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
     1.9 +    fun bisim_const T = Const (@{const_name bisim}, [iter_T, T, T] ---> bool_T)
    1.10      fun nth_sub_bisim x n nth_T =
    1.11        (if is_codatatype ctxt nth_T then bisim_const nth_T $ n_var_minus_1
    1.12         else HOLogic.eq_const nth_T)