changeset 57303 | 498a62e65f5f |
parent 56945 | 3d1ead21a055 |
child 57397 | 5004aca20821 |
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 24 13:48:14 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 24 13:48:14 2014 +0200 @@ -239,7 +239,7 @@ let fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else (); - val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd); + 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