# HG changeset patch # User blanchet # Date 1287758755 -7200 # Node ID 87edcef4fab04b1f9e84686f352d106944456107 # Parent f167beebb5277e9faeab042af1b145b2b91f4505 compile diff -r f167beebb527 -r 87edcef4fab0 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Oct 22 16:37:11 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Oct 22 16:45:55 2010 +0200 @@ -37,7 +37,7 @@ open Metis_Translate open Sledgehammer_Util open Sledgehammer_Filter -open Sledgehammer_Translate +open Sledgehammer_ATP_Translate type minimize_command = string list -> string type metis_params =