# HG changeset patch
# User blanchet
# Date 1437061116 -7200
# Node ID e3f52a15c6edb5f618d722a203eb6a5eaec86841
# Parent  a2a3766890821ac49d9f40cd5fe356c3dc5c991d
generalized generic translation function

diff -r a2a376689082 -r e3f52a15c6ed src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Jul 16 17:36:38 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Jul 16 17:38:36 2015 +0200
@@ -368,7 +368,8 @@
     and massage_mutual_fun bound_Ts U T t =
       (case t of
         Const (@{const_name comp}, _) $ t1 $ t2 =>
-        mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2)
+        if has_call t2 then massage_mutual_fun bound_Ts U T t
+        else mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, t2)
       | _ =>
         let
           val j = Term.maxidx_of_term t + 1;