try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);
(* Title: ZF/Resid/ROOT.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
Executes the Residuals example.
This is a proof of the Church-Rosser Theorem for the untyped lambda-calculus.
By Ole Rasmussen, following the Coq proof given in
Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development.
J. Functional Programming 4(3) 1994, 371-394.
*)
use_thys ["Confluence"];