--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:34 2011 +0200
@@ -17,6 +17,7 @@
datatype reconstructor =
Metis |
MetisFT |
+ MetisX |
SMT of string
datatype play =
@@ -68,6 +69,7 @@
datatype reconstructor =
Metis |
MetisFT |
+ MetisX |
SMT of string
datatype play =
@@ -253,6 +255,7 @@
fun reconstructor_name Metis = "metis"
| reconstructor_name MetisFT = "metisFT"
+ | reconstructor_name MetisX = "metisX"
| reconstructor_name (SMT _) = "smt"
fun reconstructor_settings (SMT settings) = settings
@@ -1023,7 +1026,7 @@
else
if member (op =) qs Show then "show" else "have")
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
- val reconstructor = if full_types then MetisFT else Metis
+ val reconstructor = if full_types then MetisX else Metis
fun do_facts (ls, ss) =
reconstructor_command reconstructor 1 1
(ls |> sort_distinct (prod_ord string_ord int_ord),