diff -r 3d44892ac0d6 -r f30e941b4512 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 13 16:22:18 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 13 16:40:06 2012 +0100
@@ -476,11 +476,11 @@
     pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u)
 
 val combinator_table =
-  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
-   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
-   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
-   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
-   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
+  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
+   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),
+   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),
+   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),
+   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]
 
 fun uncombine_term thy =
   let