src/HOL/TPTP/ROOT.ML
changeset 48297 dcf3160376ae
parent 48284 a3cb8901d60c
--- a/src/HOL/TPTP/ROOT.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/ROOT.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -8,8 +8,8 @@
 
 use_thys [
   "ATP_Theory_Export",
+  "MaSh_Eval",
   "MaSh_Export",
-  "MaSh_Import",
   "TPTP_Interpret",
   "THF_Arith"
 ];