changeset 53833 | ff09afd47b34 |
parent 53832 | bde758ba3029 |
child 53835 | 687116951569 |
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Tue Sep 24 19:15:49 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Tue Sep 24 19:15:50 2013 +0200 @@ -219,8 +219,7 @@ fld end; -fun massage_direct_corec_call ctxt has_call raw_massage_call U t = - massage_let_if ctxt has_call raw_massage_call U t; +val massage_direct_corec_call = massage_let_if; fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t = let