src/Tools/Code/code_preproc.ML
changeset 74561 8e6c973003c8
parent 74282 c2ee8d993d6a
child 75353 05f7f5454cb6
--- a/src/Tools/Code/code_preproc.ML	Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Tools/Code/code_preproc.ML	Wed Oct 20 18:13:17 2021 +0200
@@ -100,7 +100,6 @@
 (
   type T = thmproc;
   val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
-  val extend = I;
   val merge = merge_thmproc;
 );
 
@@ -319,7 +318,6 @@
 (
   type T = string list option;
   val empty = SOME [];
-  val extend = I;
   fun merge (NONE, _) = NONE
     | merge (_, NONE) = NONE
     | merge (SOME cs1, SOME cs2) = SOME (Library.merge (op =) (cs1, cs2));