aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2020-05-25 19:33:23 +0200
committerJosh Chen2020-05-25 19:33:49 +0200
commitf97d71514a309c212d3b20e560ce6482df0dd7ea (patch)
treefb4c2f966a1b70655d6aeb4d65b1e7904275b8cb
parent60f32406e8c9712c0689d54a3dd4f8e17d310d52 (diff)
fix implicits table merge mistake
-rw-r--r--spartan/core/implicits.ML2
1 files changed, 1 insertions, 1 deletions
diff --git a/spartan/core/implicits.ML b/spartan/core/implicits.ML
index 04fc825..4d73c8d 100644
--- a/spartan/core/implicits.ML
+++ b/spartan/core/implicits.ML
@@ -11,7 +11,7 @@ structure Defs = Generic_Data (
type T = (term * term) Symtab.table
val empty = Symtab.empty
val extend = I
- val merge = Symtab.merge (Term.aconv o #1)
+ val merge = Symtab.merge (Term.aconv o apply2 #1)
)
val implicit_defs = Defs.get o Context.Proof