src/HOL/ex/sledgehammer_tactics.ML
changeset 44651 5d6a11e166cf
parent 44625 4a1132815a70
child 45514 973bb7846505
     1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Fri Sep 02 14:43:20 2011 +0200
     1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Fri Sep 02 14:43:20 2011 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4  fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
     1.5    case run_atp override_params relevance_override i i ctxt th of
     1.6      SOME facts =>
     1.7 -    Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
     1.8 +    Metis_Tactic.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
     1.9    | NONE => Seq.empty
    1.10  
    1.11  fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =