generalized generic translation function
authorblanchet
Thu Jul 16 17:38:36 2015 +0200 (2015-07-16)
changeset 60739e3f52a15c6ed
parent 60738 a2a376689082
child 60740 c0f6d90d0ae4
generalized generic translation function
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Jul 16 17:36:38 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Jul 16 17:38:36 2015 +0200
     1.3 @@ -368,7 +368,8 @@
     1.4      and massage_mutual_fun bound_Ts U T t =
     1.5        (case t of
     1.6          Const (@{const_name comp}, _) $ t1 $ t2 =>
     1.7 -        mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2)
     1.8 +        if has_call t2 then massage_mutual_fun bound_Ts U T t
     1.9 +        else mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, t2)
    1.10        | _ =>
    1.11          let
    1.12            val j = Term.maxidx_of_term t + 1;