# HG changeset patch
# User blanchet
# Date 1282142014 -7200
# Node ID 09fe051f2782b7855e8eaa62ef53e4ca3ba90b7c
# Parent  c9f2b1a91276111809b34463a076d2ea0a7756d5
tuning

diff -r c9f2b1a91276 -r 09fe051f2782 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Wed Aug 18 12:26:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Wed Aug 18 16:33:34 2010 +0200
@@ -18,6 +18,7 @@
 structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE =
 struct
 
+open ATP_Systems
 open Sledgehammer_Util
 open Sledgehammer_Fact_Filter
 open Sledgehammer_Proof_Reconstruct
@@ -113,7 +114,8 @@
     val (_, hyp_ts, concl_t) = strip_subgoal goal i
     val explicit_apply =
       not (forall (Meson.is_fol_term thy)
-                  (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs))
+                  (concl_t :: hyp_ts @
+                   maps (map prop_of o snd) name_thms_pairs))
     fun do_test timeout =
       test_theorems params prover explicit_apply timeout i state
     val timer = Timer.startRealTimer ()