--- a/src/HOL/TPTP/ROOT.ML Mon Jan 23 17:40:32 2012 +0100 +++ b/src/HOL/TPTP/ROOT.ML Mon Jan 23 17:40:32 2012 +0100 @@ -7,7 +7,7 @@ *) use_thys [ - "ATP_Export" + "ATP_Theory_Export" ]; Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)