diff -r 31bc296a1257 -r dd112cd72c48 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 04 12:09:53 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 04 12:09:53 2012 +0100
@@ -1982,8 +1982,7 @@
                           $ (suc_const iter_T $ Bound 0) $ n_var)
     val x_var = Var (("x", 0), T)
     val y_var = Var (("y", 0), T)
-    fun bisim_const T =
-      Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
+    fun bisim_const T = Const (@{const_name bisim}, [iter_T, T, T] ---> bool_T)
     fun nth_sub_bisim x n nth_T =
       (if is_codatatype ctxt nth_T then bisim_const nth_T $ n_var_minus_1
        else HOLogic.eq_const nth_T)