diff -r 6c8170f8849e -r ac02112a208e src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -17,7 +17,6 @@
   datatype reconstructor =
     Metis |
     MetisFT |
-    MetisX |
     SMT of string
 
   datatype play =
@@ -69,7 +68,6 @@
 datatype reconstructor =
   Metis |
   MetisFT |
-  MetisX |
   SMT of string
 
 datatype play =
@@ -255,7 +253,6 @@
 
 fun reconstructor_name Metis = "metis"
   | reconstructor_name MetisFT = "metisFT"
-  | reconstructor_name MetisX = "metisX"
   | reconstructor_name (SMT _) = "smt"
 
 fun reconstructor_settings (SMT settings) = settings