src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
changeset 53833 ff09afd47b34
parent 53832 bde758ba3029
child 53835 687116951569
equal deleted inserted replaced
53832:bde758ba3029 53833:ff09afd47b34
   217       | _ => f t)
   217       | _ => f t)
   218   in
   218   in
   219     fld
   219     fld
   220   end;
   220   end;
   221 
   221 
   222 fun massage_direct_corec_call ctxt has_call raw_massage_call U t =
   222 val massage_direct_corec_call = massage_let_if;
   223   massage_let_if ctxt has_call raw_massage_call U t;
       
   224 
   223 
   225 fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
   224 fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
   226   let
   225   let
   227     val typof = curry fastype_of1 bound_Ts;
   226     val typof = curry fastype_of1 bound_Ts;
   228     val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
   227     val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)