diff -r c3b3517ef4ba -r 069f6b2c5a07 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Mon Aug 16 11:24:12 2021 +0200 +++ b/src/Pure/Isar/calculation.ML Mon Aug 16 11:49:39 2021 +0200 @@ -33,7 +33,7 @@ structure Data = Generic_Data ( type T = (thm Item_Net.T * thm Item_Net.T) * calculation option; - val empty = ((Thm.elim_rules, Thm.full_rules), NONE); + val empty = ((Thm.item_net_elim, Thm.item_net), NONE); val extend = I; fun merge (((trans1, sym1), _), ((trans2, sym2), _)) = ((Item_Net.merge (trans1, trans2), Item_Net.merge (sym1, sym2)), NONE);