src/HOL/ROOT.ML

replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
minor tuning according to Isabelle coding conventions;

(* Classical Higher-order Logic -- batteries included *)

use_thy "Complex_Main";

val HOL_proofs = ! Proofterm.proofs;