diff options
| author | Josh Chen | 2020-05-25 19:33:23 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-25 19:33:49 +0200 |
| commit | f97d71514a309c212d3b20e560ce6482df0dd7ea (patch) | |
| tree | fb4c2f966a1b70655d6aeb4d65b1e7904275b8cb | |
| parent | 60f32406e8c9712c0689d54a3dd4f8e17d310d52 (diff) | |
fix implicits table merge mistake
| -rw-r--r-- | spartan/core/implicits.ML | 2 |
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 |