diff --git a/tools/autocorres/AutoCorres.thy b/tools/autocorres/AutoCorres.thy index 531b921d5..e3b596e0f 100644 --- a/tools/autocorres/AutoCorres.thy +++ b/tools/autocorres/AutoCorres.thy @@ -24,8 +24,8 @@ imports "Lib.OptionMonadWP" "Lib.Apply_Trace" AutoCorresSimpset - "Lib.MkTermAntiquote" - "Lib.TermPatternAntiquote" + "ML_Utils.MkTermAntiquote" + "ML_Utils.TermPatternAntiquote" keywords "autocorres" :: thy_decl begin diff --git a/tools/c-parser/CTranslation.thy b/tools/c-parser/CTranslation.thy index bdec639fb..1b651654a 100644 --- a/tools/c-parser/CTranslation.thy +++ b/tools/c-parser/CTranslation.thy @@ -11,7 +11,7 @@ imports "StaticFun" "IndirectCalls" "ModifiesProofs" - "Lib.MLUtils" + "ML_Utils.MLUtils" "HOL-Eisbach.Eisbach" keywords "cond_sorry_modifies_proofs" diff --git a/tools/c-parser/ROOT b/tools/c-parser/ROOT index c83a98b47..7af1bcea7 100644 --- a/tools/c-parser/ROOT +++ b/tools/c-parser/ROOT @@ -16,6 +16,7 @@ session CParser = "Simpl-VCG" + sessions "HOL-Library" "Lib" + "ML_Utils" directories "umm_heap" "umm_heap/$L4V_ARCH"