changeset 74561 | 8e6c973003c8 |
parent 69593 | 3dda49e08b9d |
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Oct 20 17:11:46 2021 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Oct 20 18:13:17 2021 +0200 @@ -22,7 +22,6 @@ ( type T = (term * term) Item_Net.T; val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst); - val extend = I; val merge = Item_Net.merge; )