diff -r fef33067272b -r 2477286fcc7e src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Sat Aug 18 00:22:22 2007 +0200 +++ b/src/HOL/ATP_Linkup.thy Sat Aug 18 13:32:18 2007 +0200 @@ -102,7 +102,7 @@ oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *} use "Tools/res_atp_methods.ML" -setup ResAtpMethods.ResAtps_setup +setup ResAtpMethods.setup subsection {* The Metis prover *}