src/HOL/Tools/Transfer/transfer.ML
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,