src/Pure/thm.ML
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));
 );