src/Pure/Isar/calculation.ML
changeset 74152 069f6b2c5a07
parent 74149 9e73600ec75d
child 74183 af81e4a307be
--- 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);