1.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 13 16:22:18 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 13 16:40:06 2012 +0100
     1.3 @@ -476,11 +476,11 @@
     1.4      pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u)
     1.5  
     1.6  val combinator_table =
     1.7 -  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
     1.8 -   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
     1.9 -   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
    1.10 -   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
    1.11 -   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
    1.12 +  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
    1.13 +   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),
    1.14 +   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),
    1.15 +   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),
    1.16 +   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]
    1.17  
    1.18  fun uncombine_term thy =
    1.19    let