diff -r 902ab51dd12a -r 788c66a40b32 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:03 2012 +0200
@@ -5,7 +5,7 @@
 header {* MaSh Exporter *}
 
 theory MaSh_Export
-imports ATP_Theory_Export
+imports Complex_Main
 uses "mash_export.ML"
 begin