src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 35826 1590abc3d42a
parent 35592 768d17f54125
child 35865 2f8fb5242799
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Mar 17 18:16:31 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Mar 17 19:26:05 2010 +0100
     1.3 @@ -263,7 +263,7 @@
     1.4              val _ = register birth_time death_time (Thread.self (), desc);
     1.5              val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
     1.6              val message = #message (prover (! timeout) problem)
     1.7 -              handle Res_HOL_Clause.TOO_TRIVIAL =>   (* FIXME !? *)
     1.8 +              handle Sledgehammer_HOL_Clause.TOO_TRIVIAL =>   (* FIXME !? *)
     1.9                    "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
    1.10                  | ERROR msg => ("Error: " ^ msg);
    1.11              val _ = unregister message (Thread.self ());