changeset 74561 | 8e6c973003c8 |
parent 74525 | c960bfcb91db |
child 74577 | d4829a7333e2 |
--- a/src/Pure/thm.ML Wed Oct 20 17:11:46 2021 +0200 +++ b/src/Pure/thm.ML Wed Oct 20 18:13:17 2021 +0200 @@ -922,7 +922,6 @@ classes; (*type classes within the logic*) val empty : T = (Name_Space.empty_table Markup.oracleN, empty_classes); - val extend = I; fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T = (Name_Space.merge_tables (oracles1, oracles2), merge_classes (sorts1, sorts2)); );