# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 494fde2077065f3dd85970741bf65a4802570a6f
# Parent  0ab7265f659f3e9ebff67701e02932b19819680f
don't translate new Skolemizer assumptions in new Metis

diff -r 0ab7265f659f -r 494fde207706 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -362,9 +362,10 @@
               #> fst #> maps (map (zero_var_indexes o snd)))
       val (old_skolems, props) =
         fold_rev (fn clause => fn (old_skolems, props) =>
-                     conceal_old_skolem_terms (length clauses) old_skolems
-                                              (prop_of clause)
-                     ||> (fn prop => prop :: props))
+                     clause |> prop_of |> Logic.strip_imp_concl
+                            |> conceal_old_skolem_terms (length clauses)
+                                                        old_skolems
+                            ||> (fn prop => prop :: props))
              clauses ([], [])
       val (atp_problem, _, _, _, _, _, sym_tab) =
         prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply