author | blanchet |
Fri, 27 Sep 2013 19:30:49 +0200 | |
changeset 53960 | 949cef2095e2 |
parent 53959 | 024fadbd03f0 |
child 53961 | 16d9ecdf519a |
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Fri Sep 27 17:57:45 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Fri Sep 27 19:30:49 2013 +0200 @@ -368,8 +368,10 @@ | _ => ill_formed_corec_call ctxt t) else build_map_Inl (T, U) $ t) bound_Ts; + + val T = fastype_of1 (bound_Ts, t); in - massage_call bound_Ts U (fastype_of1 (bound_Ts, t)) t + if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t end; fun expand_ctr_term ctxt s Ts t =