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;