# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 283114859d6c79366db3312219bbf4c664199cae
# Parent  db5fb1d4df425b4d240e19d9e9ea397d45592cc5
conceal old Skolems in new Metis

diff -r db5fb1d4df42 -r 283114859d6c 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
@@ -360,14 +360,19 @@
               #> rpair ctxt
               #-> Monomorph.monomorph Monomorph.all_schematic_consts_of
               #> 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))
+             clauses ([], [])
       val (atp_problem, _, _, _, _, _, sym_tab) =
         prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
-                            false false (map prop_of clauses) @{prop False} []
+                            false false props @{prop False} []
       val axioms =
         atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
     in
-      (MX, sym_tab,
-       {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)})
+      (MX, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems})
     end
   | prepare_metis_problem ctxt mode _ conj_clauses fact_clauses =
     let