equal
deleted
inserted
replaced
1113 xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, |
1113 xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, |
1114 xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...}, lthy)) = |
1114 xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...}, lthy)) = |
1115 fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs |
1115 fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs |
1116 no_defs_lthy0; |
1116 no_defs_lthy0; |
1117 |
1117 |
|
1118 val time = time lthy; |
1118 val timer = time (Timer.startRealTimer ()); |
1119 val timer = time (Timer.startRealTimer ()); |
1119 |
1120 |
1120 val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As; |
1121 val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As; |
1121 val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs; |
1122 val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs; |
1122 |
1123 |