# HG changeset patch
# User blanchet
# Date 1425561945 -3600
# Node ID 7892ffd1c39d691681f81d8f4961a6eb380e0f72
# Parent  e41ac095f99d4377a14b9a5bf7af5422ab521695
deal better with corecursion through functions

diff -r e41ac095f99d -r 7892ffd1c39d src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 05 13:44:41 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 05 14:25:45 2015 +0100
@@ -288,13 +288,16 @@
 
     val build_map_Inl = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd);
 
-    fun massage_mutual_call bound_Ts U T t =
-      if has_call t then
-        (case try dest_sumT U of
-          SOME (U1, U2) => if U1 = T then raw_massage_call bound_Ts T U2 t else invalid_map ctxt t
-        | NONE => invalid_map ctxt t)
-      else
-        build_map_Inl (T, U) $ t;
+    fun massage_mutual_call bound_Ts (Type (@{type_name fun}, [_, U2]))
+        (Type (@{type_name fun}, [T1, T2])) t =
+        Abs (Name.uu, T1, massage_mutual_call bound_Ts U2 T2 (incr_boundvars 1 t $ Bound 0))
+      | massage_mutual_call bound_Ts U T t =
+        if has_call t then
+          (case try dest_sumT U of
+            SOME (U1, U2) => if U1 = T then raw_massage_call bound_Ts T U2 t else invalid_map ctxt t
+          | NONE => invalid_map ctxt t)
+        else
+          build_map_Inl (T, U) $ t;
 
     fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t =
         (case try (dest_map ctxt s) t of
@@ -321,8 +324,8 @@
         mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2)
       | _ =>
         let
-          val var = Var ((Name.uu, Term.maxidx_of_term t + 1),
-            domain_type (fastype_of1 (bound_Ts, t)));
+          val j = Term.maxidx_of_term t + 1;
+          val var = Var ((Name.uu, j), domain_type (fastype_of1 (bound_Ts, t)));
         in
           Term.lambda var (Term.incr_boundvars 1 (massage_call bound_Ts U T (betapply (t, var))))
         end)