src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 33316 6a72af4e84b8
parent 33312 6ca8a7984fd9
child 33522 737589bb9bb8
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 29 16:34:44 2009 +0100
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 29 16:59:12 2009 +0100
     1.3 @@ -264,7 +264,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 ResHolClause.TOO_TRIVIAL =>   (* FIXME !? *)
     1.8 +              handle Res_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 ());