--- a/src/HOL/Tools/Sledgehammer/metis_translate.ML Wed Sep 29 23:06:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML Wed Sep 29 23:24:31 2010 +0200
@@ -627,7 +627,8 @@
let
val thy = ProofContext.theory_of ctxt
val (old_skolems, (mlits, types_sorts)) =
- th |> prop_of |> conceal_old_skolem_terms j old_skolems
+ th |> prop_of |> Logic.strip_imp_concl
+ |> conceal_old_skolem_terms j old_skolems
||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode)
in
if is_conjecture then