diff -r 2e10a36b8d46 -r 3298b7a2795a src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 21 12:34:50 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 21 15:12:03 2014 +0100
@@ -404,7 +404,7 @@
 (* These are ignored anyway by the relevance filter (unless they appear in
    higher-order places) but not by the monomorphizer. *)
 val atp_logical_consts =
-  [@{const_name prop}, @{const_name Pure.conjunction}, @{const_name all}, @{const_name "==>"},
+  [@{const_name Pure.prop}, @{const_name Pure.conjunction}, @{const_name all}, @{const_name "==>"},
    @{const_name "=="}, @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
    @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]