# HG changeset patch
# User blanchet
# Date 1285795471 -7200
# Node ID 40ef95149770e9dd91de05d0c5faa61842bf98a3
# Parent  74939e2afb959317c530eba0ac67f67d2a82de77
ignore Skolem assumption (if any)

diff -r 74939e2afb95 -r 40ef95149770 src/HOL/Tools/Sledgehammer/metis_translate.ML
--- 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