src/HOL/SPARK/Tools/spark_vcs.ML
changeset 74561 8e6c973003c8
parent 74396 dc73f9e6476b
child 80328 559909bd7715
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Oct 20 18:13:17 2021 +0200
@@ -58,7 +58,6 @@
         path: Path.T,
         prefix: string} option}
   val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
-  val extend = I
   fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
         {pfuns = pfuns2, type_map = type_map2, env = NONE}) =
         {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),