# HG changeset patch
# User blanchet
# Date 1280745410 -7200
# Node ID c1cf80763eff8b8cde1f81fdc01c8c1ec7f2a798
# Parent  d04aceff43cf3e81386ca7ccbd22e1a0bf72548a
fix bug with mutually recursive and nested codatatypes

diff -r d04aceff43cf -r c1cf80763eff src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Aug 01 23:15:26 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 02 12:36:50 2010 +0200
@@ -1842,7 +1842,6 @@
     val xs = datatype_constrs hol_ctxt T
     val set_T = T --> bool_T
     val iter_T = @{typ bisim_iterator}
-    val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
     val bisim_max = @{const bisim_iterator_max}
     val n_var = Var (("n", 0), iter_T)
     val n_var_minus_1 =
@@ -1851,8 +1850,10 @@
                           $ (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 nth_sub_bisim x n nth_T =
-      (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
+      (if is_codatatype thy nth_T then bisim_const nth_T $ n_var_minus_1
        else HOLogic.eq_const nth_T)
       $ select_nth_constr_arg ctxt stds x x_var n nth_T
       $ select_nth_constr_arg ctxt stds x y_var n nth_T
@@ -1865,12 +1866,12 @@
           |> foldr1 s_conj
       in List.foldr absdummy core_t arg_Ts end
   in
-    [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
+    [HOLogic.eq_const bool_T $ (bisim_const T $ n_var $ x_var $ y_var)
      $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
         $ (s_betapply []
                       (optimized_case_def hol_ctxt T bool_T (map case_func xs),
                        x_var))),
-     HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
+     HOLogic.eq_const set_T $ (bisim_const T $ bisim_max $ x_var)
      $ (Const (@{const_name insert}, T --> set_T --> set_T)
         $ x_var $ Const (@{const_name bot_class.bot}, set_T))]
     |> map HOLogic.mk_Trueprop