Permalink
Browse files

Ensure current theory is known to translator

Adds current_theory() to the type theories known by the translator
when extending. Otherwise XXX_TYPE_def:s generated by our translation
after extension won't be found. :-)
  • Loading branch information...
oskarabrahamsson authored and xrchz committed Oct 10, 2017
1 parent 0571b2d commit 1c32c711faefacaf39e87f7f2a95fd9312dc3174
Showing with 9 additions and 1 deletion.
  1. +9 −1 translator/monadic/ml_monad_translatorLib.sml
@@ -2437,9 +2437,17 @@ local
(unpack_list (unpack_pair unpack_term unpack_thm))
(unpack_list (unpack_pair unpack_term unpack_thm))
(unpack_list (unpack_pair unpack_thm unpack_thm)) th
(* Need to add the current theory to type_theories or we cannot
access definitions generated after extending! *)
val curr_thy =
case List.find (fn thy => thy = current_theory ()) tt of
NONE => [current_theory ()]
| _ => []
val _ = (EXN_TYPE_def_ref := etdr)
val _ = (EXN_TYPE := et)
val _ = (type_theories := tt)
val _ = (type_theories := tt @ curr_thy)
val _ = (exn_handles := eh)
val _ = (exn_raises := er)
val _ = (exn_functions_defs := efd)

0 comments on commit 1c32c71

Please sign in to comment.