diff -r 1403595ec38c -r 4e2d6c1e5392 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Tue May 24 10:00:38 2011 +0200
@@ -392,11 +392,11 @@
                 [typ_u, term_u] =>
                 aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u
               | _ => raise FO_TERM us
-            else if s' = predicator_base then
+            else if s' = predicator_name then
               aux (SOME @{typ bool}) [] (hd us)
-            else if s' = explicit_app_base then
+            else if s' = app_op_name then
               aux opt_T (nth us 1 :: extra_us) (hd us)
-            else if s' = type_pred_base then
+            else if s' = type_pred_name then
               @{const True} (* ignore type predicates *)
             else
               let