1if String.isPrefix "Fail: " (General.exnMessage (General.Fail "")) 2 then use "tools/configure-mosml.sml" 3else use "tools-poly/smart-configure.sml" 4 handle e => 5 if String.isPrefix "Io" (General.exnMessage e) then 6 TextIO.print 7 "\n\n** You must do\n poly < tools/smart-configure.sml\n\ 8 \** from the root HOL directory\n\n" 9 else () 10