src/HOL/Tools/BNF/bnf_lfp.ML
changeset 56192 d666cb0e4cf9
parent 56114 bc7335979247
child 56237 69a9dfe71aed
equal deleted inserted replaced
56191:159b0c88b4a4 56192:d666cb0e4cf9
  1481           end;
  1481           end;
  1482 
  1482 
  1483         val (Ibnf_consts, lthy) =
  1483         val (Ibnf_consts, lthy) =
  1484           fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
  1484           fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
  1485               fn T => fn lthy =>
  1485               fn T => fn lthy =>
  1486             define_bnf_consts Dont_Inline (user_policy Note_Some lthy) false (SOME deads)
  1486             define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads)
  1487               map_b rel_b set_bs
  1487               map_b rel_b set_bs
  1488               ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
  1488               ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
  1489           bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
  1489           bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
  1490 
  1490 
  1491         val (_, Iconsts, Iconst_defs, mk_Iconsts) = split_list4 Ibnf_consts;
  1491         val (_, Iconsts, Iconst_defs, mk_Iconsts) = split_list4 Ibnf_consts;