--- 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}]