reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
(* Title: LCF/ROOT.ML
Author: Tobias Nipkow
Copyright 1992 University of Cambridge
*)
use_thys ["LCF"];