1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Nov 16 11:16:23 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Nov 16 13:22:36 2011 +0100
     1.3 @@ -22,6 +22,7 @@
     1.4  open ATP_Util
     1.5  open ATP_Systems
     1.6  open ATP_Translate
     1.7 +open ATP_Reconstruct
     1.8  open Sledgehammer_Util
     1.9  open Sledgehammer_Filter
    1.10  open Sledgehammer_Provers
    1.11 @@ -310,7 +311,7 @@
    1.12  
    1.13  (* Sledgehammer the given subgoal *)
    1.14  
    1.15 -val default_minimize_prover = Metis_Tactic.metisN
    1.16 +val default_minimize_prover = metisN
    1.17  
    1.18  fun is_raw_param_relevant_for_minimize (name, _) =
    1.19    member (op =) params_for_minimize name