src/Pure/Isar/class.ML
changeset 74152 069f6b2c5a07
parent 74150 de12016ffefb
child 74232 1091880266e5
--- a/src/Pure/Isar/class.ML	Mon Aug 16 11:24:12 2021 +0200
+++ b/src/Pure/Isar/class.ML	Mon Aug 16 11:49:39 2021 +0200
@@ -227,7 +227,7 @@
         make_class_data (((map o apply2) fst params, base_sort,
           base_morph, export_morph, Option.map Thm.trim_context some_assm_intro,
           Thm.trim_context of_class, Option.map Thm.trim_context some_axiom),
-          (Thm.full_rules, operations)))
+          (Thm.item_net, operations)))
       #> fold (curry Graph.add_edge class) sups;
   in Class_Data.map add_class thy end;