changeset 45515 | 5d6a11e166cf |
parent 45455 | 0b107d11f634 |
child 45591 | f3a8c19708c8 |
1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 02 14:43:20 2011 +0200 1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 02 14:43:20 2011 +0200 1.3 @@ -299,7 +299,7 @@ 1.4 1.5 (* Sledgehammer the given subgoal *) 1.6 1.7 -val default_minimize_prover = Metis_Tactics.metisN 1.8 +val default_minimize_prover = Metis_Tactic.metisN 1.9 1.10 val is_raw_param_relevant_for_minimize = 1.11 member (op =) params_for_minimize o fst o unalias_raw_param