changeset 74561 | 8e6c973003c8 |
parent 74545 | 6c123914883a |
child 79274 | fb8ed7fbb537 |
--- a/src/HOL/Tools/Transfer/transfer.ML Wed Oct 20 17:11:46 2021 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Wed Oct 20 18:13:17 2021 +0200 @@ -94,7 +94,6 @@ relator_eq_raw = Thm.item_net, relator_domain = Thm.item_net, pred_data = Symtab.empty } - val extend = I fun merge ( { transfer_raw = t1, known_frees = k1, compound_lhs = l1,