1fun emacs_hol_mode_loaded () =
2   ["HOL_Interactive", "Meta",
3  "Array", "ArraySlice", "BinIO", "BinPrimIO", "Bool", "Byte",
4  "CharArray", "CharArraySlice", "Char", "CharVector",
5  "CharVectorSlice", "CommandLine.name", "Date", "General", "IEEEReal",
6  "Int", "IO", "LargeInt", "LargeReal", "LargeWord", "List", "ListPair",
7  "Math", "Option", "OS", "Position", "Real", "StringCvt", "String",
8  "Substring", "TextIO", "TextPrimIO", "Text", "Timer", "Time",
9  "VectorSlice", "Vector", "Word8Array", "Word8ArraySlice",
10  "Word8Vector", "Word8VectorSlice", "Word8", "Word"] @ (Meta.loaded());
11