src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
changeset 54838 16511f84913c
parent 54836 47857a79bdad
child 55168 948e8b7ea82f
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Dec 20 16:22:10 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Dec 20 20:36:38 2013 +0100
@@ -197,7 +197,7 @@
 val arith_methodss =
   [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
     Metis_Method], [Meson_Method]]
-val datatype_methodss = [[Auto_Method, Simp_Method, Blast_Method]]
+val datatype_methodss = [[Simp_Size_Method, Simp_Method]]
 val metislike_methodss =
   [[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
     Force_Method], [Meson_Method]]