--- 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