Skip to content
Permalink
Browse files

Stop assuming term eqtype in basis_ffiLib

  • Loading branch information...
xrchz committed Feb 19, 2019
1 parent 98d01f3 commit f203d828565dd16165d078b876491549745d0ba9
Showing with 2 additions and 2 deletions.
  1. +2 −2 basis/basis_ffiLib.sml
@@ -83,8 +83,8 @@ fun subset_basis_st st precond sets sets_thm =
)
val (subgoals,_) = tac ([],goal)
fun mk_mapping (x,y) =
if mem x to_inst then SOME (x |-> y) else
if mem y to_inst then SOME (y |-> x) else NONE
if tmem x to_inst then SOME (x |-> y) else
if tmem y to_inst then SOME (y |-> x) else NONE
fun safe_dest_eq tm =
if boolSyntax.is_eq tm then boolSyntax.dest_eq tm else
Lib.tryfind boolSyntax.dest_eq (boolSyntax.strip_disj tm)

0 comments on commit f203d82

Please sign in to comment.
You can’t perform that action at this time.