replaced ML pokes by explicit usedir -p;
prefer -q 0 for proof terms, which avoids overhead of proof promises, while exploiting implicit parallelism of internal normalization;

 (*  Title:      HOL/Import/ROOT.ML

     Author:     Sebastian Skalberg (TU Muenchen)

 *)

 use_thys ["HOL4Compat", "HOL4Syntax"];