Commit 7966637f authored by Heiko Becker's avatar Heiko Becker

Fix typing bug in HOL4 too

parent ad5170ed
......@@ -45,7 +45,7 @@ val typeMap_def = Define `
| Unop u e1 =>
let tMap_new = typeMap Gamma e1 tMap fBits in
(case FloverMapTree_find e1 tMap_new of
| SOME m_e1 => FloverMapTree_insert e m_e1 tMap
| SOME m_e1 => FloverMapTree_insert e m_e1 tMap_new
| NONE => FloverMapTree_empty)
| Binop b e1 e2 =>
let tMap1 = typeMap Gamma e1 tMap fBits in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment