diff -r d3d91422f408 -r 488046fdda59 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 16 13:19:48 2014 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 16 16:18:15 2014 +0200
@@ -48,7 +48,7 @@
     ATerm ((Metis_Name.toString s, []), [])
 
 fun hol_term_of_metis ctxt type_enc sym_tab =
-  atp_term_of_metis type_enc #> term_of_atp ctxt false sym_tab NONE
+  atp_term_of_metis type_enc #> term_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab NONE
 
 fun atp_literal_of_metis type_enc (pos, atom) =
   atom |> Metis_Term.Fn |> atp_term_of_metis type_enc
@@ -65,7 +65,7 @@
   Metis_Thm.clause
   #> Metis_LiteralSet.toList
   #> atp_clause_of_metis type_enc
-  #> prop_of_atp ctxt false sym_tab
+  #> prop_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab
   #> singleton (polish_hol_terms ctxt concealed)
 
 fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms =