1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 29 11:14:52 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 29 11:20:05 2010 +0200
     1.3 @@ -324,7 +324,7 @@
     1.4        NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
     1.5      | SOME _ => (message, SH_FAIL (time_isa, time_atp))
     1.6    end
     1.7 -  handle Metis_Clauses.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
     1.8 +  handle ATP_Manager.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
     1.9         | ERROR msg => ("error: " ^ msg, SH_ERROR)
    1.10         | TimeLimit.TimeOut => ("timeout", SH_ERROR)
    1.11