1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Nov 18 11:47:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Nov 18 11:47:12 2011 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4      lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
     1.5  
     1.6  fun polish_hol_terms ctxt (lifted, old_skolems) =
     1.7 -  map (reveal_lambda_lifted lifted #> reveal_old_skolem_terms old_skolems)
     1.8 +  map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems)
     1.9    #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
    1.10  
    1.11  fun hol_clause_from_metis ctxt type_enc sym_tab concealed =