optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
saves 2 sec per Sledgehammer invocation on my laptop!
(* Title: FOLP/ROOT.ML
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Modifed version of Lawrence Paulson's FOL that contains proof terms.
Presence of unknown proof term means that matching does not behave as expected.
*)
use_thys ["FOLP"];