| changeset 74561 | 8e6c973003c8 |
| parent 71214 | 5727bcc3c47c |
| child 76054 | a4b47c684445 |
--- a/src/HOL/Tools/inductive.ML Wed Oct 20 17:11:46 2021 +0200 +++ b/src/HOL/Tools/inductive.ML Wed Oct 20 18:13:17 2021 +0200 @@ -214,7 +214,6 @@ ( type T = data; val empty = make_data (empty_infos, [], empty_equations); - val extend = I; fun merge (Data {infos = infos1, monos = monos1, equations = equations1}, Data {infos = infos2, monos = monos2, equations = equations2}) = make_data (Item_Net.merge (infos1, infos2),