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),