src/HOL/Tools/BNF/bnf_gfp.ML
changeset 56348 2653b2fdad06
parent 56346 42533f8f4729
child 56516 a13c2ccc160b
equal deleted inserted replaced
56347:6edbd4d20717 56348:2653b2fdad06
  2431         fun wit_tac thms ctxt =
  2431         fun wit_tac thms ctxt =
  2432           mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms;
  2432           mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms;
  2433 
  2433 
  2434         val (Jbnfs, lthy) =
  2434         val (Jbnfs, lthy) =
  2435           fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms =>
  2435           fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms =>
  2436               fn consts => fn lthy =>
  2436               fn consts =>
  2437             bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms)
  2437             bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms)
  2438               (SOME deads) map_b rel_b set_bs consts lthy
  2438               (SOME deads) map_b rel_b set_bs consts
  2439             |> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy)))
  2439             #> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy)))
  2440           bs tacss map_bs rel_bs set_bss wit_thmss
  2440           bs tacss map_bs rel_bs set_bss wit_thmss
  2441           ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ all_witss) ~~ map SOME Jrels)
  2441           ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ all_witss) ~~ map SOME Jrels)
  2442           lthy;
  2442           lthy;
  2443 
  2443 
  2444         val timer = time (timer "registered new codatatypes as BNFs");
  2444         val timer = time (timer "registered new codatatypes as BNFs");