src/HOL/Tools/Sledgehammer/metis_tactics.ML

 end
 
 structure Metis_Tactics : METIS_TACTICS =
 struct
 
+open Sledgehammer_Util
 open Sledgehammer_FOL_Clause
 open Sledgehammer_Fact_Preprocessor
 open Sledgehammer_HOL_Clause
 open Sledgehammer_Proof_Reconstruct
 open Sledgehammer_Fact_Filter

      (case strip_combterm_comb tm of
           (CombConst(("equal", _), _, _), tms) =>
             metis_lit pol "=" (map hol_term_to_fol_FT tms)
         | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
 
-fun literals_of_hol_thm thy mode t =
+fun literals_of_hol_term thy mode t =
       let val (lits, types_sorts) = literals_of_term thy t
       in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
 
 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
 fun metis_of_type_literals pos (TyLitVar (s, (s', _))) =

   | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
 
 fun metis_of_tfree tf =
   Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
 
-fun hol_thm_to_fol is_conjecture ctxt mode th =
-  let val thy = ProofContext.theory_of ctxt
-      val (mlits, types_sorts) =
-             (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
+fun hol_thm_to_fol is_conjecture ctxt mode j skolem_somes th =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val (skolem_somes, (mlits, types_sorts)) =
+     th |> prop_of |> kill_skolem_Eps j skolem_somes
+        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
   in
       if is_conjecture then
           (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
-           type_literals_for_types types_sorts)
+           type_literals_for_types types_sorts, skolem_somes)
       else
         let val tylits = filter_out (default_sort ctxt) types_sorts
                          |> type_literals_for_types
             val mtylits = if Config.get ctxt type_lits
                           then map (metis_of_type_literals false) tylits else []
         in
-          (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
+          (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [],
+           skolem_somes)
         end
   end;
 
 (* ARITY CLAUSE *)
 

         | NONE    =>
       case strip_prefix tfree_prefix x of
           SOME tf => mk_tfree ctxt tf
         | NONE    => error ("fol_type_to_isa: " ^ x));
 
+fun reintroduce_skolem_Eps thy skolem_somes =
+  let
+    fun aux Ts args t =
+      case t of
+        t1 $ t2 => aux Ts (aux Ts [] t2 :: args) t1
+      | Abs (s, T, t') => list_comb (Abs (s, T, aux (T :: Ts) [] t'), args)
+      | Const (s, T) =>
+        if String.isPrefix skolem_Eps_pseudo_theory s then
+          let
+            val (T', args', def') = AList.lookup (op =) skolem_somes s |> the
+          in
+            def' |> subst_free (args' ~~ args)
+                 |> map_types Type_Infer.paramify_vars
+          end
+        else
+          list_comb (t, args)
+      | t => list_comb (t, args)
+  in aux [] [] end
+
 (*Maps metis terms to isabelle terms*)
-fun fol_term_to_hol_RAW ctxt fol_tm =
+fun hol_term_from_fol_PT ctxt fol_tm =
   let val thy = ProofContext.theory_of ctxt
-      val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
+      val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^
+                                  Metis.Term.toString fol_tm)
       fun tm_to_tt (Metis.Term.Var v) =
              (case strip_prefix tvar_prefix v of
                   SOME w => Type (make_tvar w)
                 | NONE =>
               case strip_prefix schematic_var_prefix v of

             case strip_prefix fixed_var_prefix a of
                 SOME b =>
                   let val opr = Term.Free(b, HOLogic.typeT)
                   in  apply_list opr (length ts) (map tm_to_tt ts)  end
               | NONE => error ("unexpected metis function: " ^ a)
-  in  case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected"  end;
+  in
+    case tm_to_tt fol_tm of
+      Term t => t
+    | _ => error "fol_tm_to_tt: Term expected"
+  end
 
 (*Maps fully-typed metis terms to isabelle terms*)
-fun fol_term_to_hol_FT ctxt fol_tm =
-  let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
+fun hol_term_from_fol_FT ctxt fol_tm =
+  let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^
+                                  Metis.Term.toString fol_tm)
       fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
              (case strip_prefix schematic_var_prefix v of
                   SOME w =>  mk_var(w, dummyT)
                 | NONE   => mk_var(v, dummyT))
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =

            (case strip_prefix const_prefix x of
                 SOME c => Const (invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix fixed_var_prefix x of
                 SOME v => Free (v, fol_type_to_isa ctxt ty)
-              | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
+              | NONE => error ("hol_term_from_fol_FT bad constant: " ^ x))
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
             cvt tm1 $ cvt tm2
         | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
             cvt tm1 $ cvt tm2
         | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)

            (case strip_prefix const_prefix x of
                 SOME c => Const (invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix fixed_var_prefix x of
                 SOME v => Free (v, dummyT)
-              | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
-                  fol_term_to_hol_RAW ctxt t))
-        | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t);
-            fol_term_to_hol_RAW ctxt t)
-  in  cvt fol_tm   end;
-
-fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt
-  | fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt
-  | fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt;
-
-fun fol_terms_to_hol ctxt mode fol_tms =
-  let val ts = map (fol_term_to_hol ctxt mode) fol_tms
+              | NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x);
+                  hol_term_from_fol_PT ctxt t))
+        | cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t);
+            hol_term_from_fol_PT ctxt t)
+  in fol_tm |> cvt end
+
+fun hol_term_from_fol FT = hol_term_from_fol_FT
+  | hol_term_from_fol _ = hol_term_from_fol_PT
+
+fun hol_terms_from_fol ctxt mode skolem_somes fol_tms =
+  let val thy = ProofContext.theory_of ctxt
+      val ts = map (hol_term_from_fol mode ctxt) fol_tms
       val _ = trace_msg (fn () => "  calling type inference:")
       val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
-      val ts' = infer_types ctxt ts;
+      val ts' =
+        ts |> map (reintroduce_skolem_Eps thy skolem_somes) |> infer_types ctxt
       val _ = app (fn t => trace_msg
                     (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
                               "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
                   ts'
   in  ts'  end;

 (* INFERENCE RULE: AXIOM *)
 fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
     (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
 
 (* INFERENCE RULE: ASSUME *)
-fun assume_inf ctxt mode atm =
+fun assume_inf ctxt mode skolem_somes atm =
   inst_excluded_middle
     (ProofContext.theory_of ctxt)
-    (singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm));
+    (singleton (hol_terms_from_fol ctxt mode skolem_somes) (Metis.Term.Fn atm))
 
 (* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
    them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
    that new TVars are distinct and that types can be inferred from terms.*)
-fun inst_inf ctxt mode thpairs fsubst th =
+fun inst_inf ctxt mode skolem_somes thpairs fsubst th =
   let val thy = ProofContext.theory_of ctxt
       val i_th   = lookth thpairs th
       val i_th_vars = Term.add_vars (prop_of i_th) []
       fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
       fun subst_translation (x,y) =
             let val v = find_var x
-                val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
+                (* We call "reintroduce_skolem_Eps" and "infer_types" below. *)
+                val t = hol_term_from_fol mode ctxt y
             in  SOME (cterm_of thy (Var v), t)  end
             handle Option =>
                 (trace_msg (fn() => "List.find failed for the variable " ^ x ^
                                        " in " ^ Display.string_of_thm ctxt i_th);
                  NONE)

                 SOME _ => NONE          (*type instantiations are forbidden!*)
               | NONE   => SOME (a,t)    (*internal Metis var?*)
       val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
       val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
       val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
-      val tms = infer_types ctxt rawtms;
+      val tms = rawtms |> map (reintroduce_skolem_Eps thy skolem_somes)
+                       |> infer_types ctxt
       val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
       val substs' = ListPair.zip (vars, map ctm_of tms)
       val _ = trace_msg (fn () =>
         cat_lines ("subst_translations:" ::
           (substs' |> map (fn (x, y) =>
             Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
             Syntax.string_of_term ctxt (term_of y)))));
-  in  cterm_instantiate substs' i_th end
+  in cterm_instantiate substs' i_th end
   handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg)
        | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^
-                             "\n(Perhaps you want to try \"metisFT\".)")
+                             "\n(Perhaps you want to try \"metisFT\" if you \
+                             \haven't done so already.)")
 
 (* INFERENCE RULE: RESOLVE *)
 
 (*Like RSN, but we rename apart only the type variables. Vars here typically have an index
   of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars

       case distinct Thm.eq_thm ths of
         [th] => th
       | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
   end;
 
-fun resolve_inf ctxt mode thpairs atm th1 th2 =
+fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
   let
     val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
     val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
     val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   in
     if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
     else if is_TrueI i_th2 then i_th1
     else
       let
-        val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
+        val i_atm = singleton (hol_terms_from_fol ctxt mode skolem_somes)
+                              (Metis.Term.Fn atm)
         val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
         val prems_th1 = prems_of i_th1
         val prems_th2 = prems_of i_th2
         val index_th1 = get_index (mk_not i_atm) prems_th1
               handle Empty => error "Failed to find literal in th1"

 
 (* INFERENCE RULE: REFL *)
 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
 
-fun refl_inf ctxt mode t =
+fun refl_inf ctxt mode skolem_somes t =
   let val thy = ProofContext.theory_of ctxt
-      val i_t = singleton (fol_terms_to_hol ctxt mode) t
+      val i_t = singleton (hol_terms_from_fol ctxt mode skolem_somes) t
       val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
       val c_t = cterm_incr_types thy refl_idx i_t
   in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
 
 fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0  (*equality has no type arguments*)
   | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
   | get_ty_arg_size _ _ = 0;
 
 (* INFERENCE RULE: EQUALITY *)
-fun equality_inf ctxt mode (pos, atm) fp fr =
+fun equality_inf ctxt mode skolem_somes (pos, atm) fp fr =
   let val thy = ProofContext.theory_of ctxt
       val m_tm = Metis.Term.Fn atm
-      val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
+      val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolem_somes [m_tm, fr]
       val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
       fun replace_item_list lx 0 (_::ls) = lx::ls
         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
       fun path_finder_FO tm [] = (tm, Term.Bound 0)
         | path_finder_FO tm (p::ps) =

         (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   in  cterm_instantiate eq_terms subst'  end;
 
 val factor = Seq.hd o distinct_subgoals_tac;
 
-fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th)
-  | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm
-  | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) =
-      factor (inst_inf ctxt mode thpairs f_subst f_th1)
-  | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
-      factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
-  | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm
-  | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
-      equality_inf ctxt mode f_lit f_p f_r;
+fun step ctxt mode skolem_somes thpairs p =
+  case p of
+    (fol_th, Metis.Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
+  | (_, Metis.Proof.Assume f_atm) => assume_inf ctxt mode skolem_somes f_atm
+  | (_, Metis.Proof.Subst (f_subst, f_th1)) =>
+    factor (inst_inf ctxt mode skolem_somes thpairs f_subst f_th1)
+  | (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =>
+    factor (resolve_inf ctxt mode skolem_somes thpairs f_atm f_th1 f_th2)
+  | (_, Metis.Proof.Refl f_tm) => refl_inf ctxt mode skolem_somes f_tm
+  | (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =>
+    equality_inf ctxt mode skolem_somes f_lit f_p f_r
 
 fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
 
-fun translate _ _ thpairs [] = thpairs
-  | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
+(* TODO: use "fold" instead *)
+fun translate _ _ _ thpairs [] = thpairs
+  | translate ctxt mode skolem_somes thpairs ((fol_th, inf) :: infpairs) =
       let val _ = trace_msg (fn () => "=============================================")
           val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
           val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
-          val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
+          val th = Meson.flexflex_first_order (step ctxt mode skolem_somes
+                                                    thpairs (fol_th, inf))
           val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
           val _ = trace_msg (fn () => "=============================================")
           val n_metis_lits =
             length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
       in
           if nprems_of th = n_metis_lits then ()
           else error "Metis: proof reconstruction has gone wrong";
-          translate mode ctxt ((fol_th, th) :: thpairs) infpairs
+          translate ctxt mode skolem_somes ((fol_th, th) :: thpairs) infpairs
       end;
 
 (*Determining which axiom clauses are actually used*)
 fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
   | used_axioms _ _ = NONE;

 (* Logic maps manage the interface between HOL and first-order logic.        *)
 (* ------------------------------------------------------------------------- *)
 
 type logic_map =
   {axioms: (Metis.Thm.thm * thm) list,
-   tfrees: type_literal list};
+   tfrees: type_literal list,
+   skolem_somes: (string * (typ * term list * term)) list}
 
 fun const_in_metis c (pred, tm_list) =
   let
     fun in_mterm (Metis.Term.Var _) = false
       | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list

     |> type_literals_for_types
   end;
 
 (*transform isabelle type / arity clause to metis clause *)
 fun add_type_thm [] lmap = lmap
-  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees} =
-      add_type_thm cls {axioms = (mth, ith) :: axioms,
-                        tfrees = tfrees}
+  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolem_somes} =
+      add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
+                        skolem_somes = skolem_somes}
 
 (*Insert non-logical axioms corresponding to all accumulated TFrees*)
-fun add_tfrees {axioms, tfrees} : logic_map =
-     {axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
-      tfrees = tfrees};
+fun add_tfrees {axioms, tfrees, skolem_somes} : logic_map =
+     {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
+               axioms,
+      tfrees = tfrees, skolem_somes = skolem_somes}
 
 fun string_of_mode FO = "FO"
   | string_of_mode HO = "HO"
   | string_of_mode FT = "FT"
 
 (* Function to generate metis clauses, including comb and type clauses *)
 fun build_map mode0 ctxt cls ths =
   let val thy = ProofContext.theory_of ctxt
       (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
       fun set_mode FO = FO
-        | set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO
+        | set_mode HO =
+          if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO
+          else HO
         | set_mode FT = FT
       val mode = set_mode mode0
       (*transform isabelle clause to metis clause *)
-      fun add_thm is_conjecture ith {axioms, tfrees} : logic_map =
-        let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
+      fun add_thm is_conjecture ith {axioms, tfrees, skolem_somes} : logic_map =
+        let
+          val (mth, tfree_lits, skolem_somes) =
+            hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolem_somes
+                           ith
         in
            {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
-            tfrees = union (op =) tfree_lits tfrees}
+            tfrees = union (op =) tfree_lits tfrees,
+            skolem_somes = skolem_somes}
         end;
-      val lmap0 = fold (add_thm true) cls {axioms = [], tfrees = init_tfrees ctxt}
-      val lmap = fold (add_thm false) ths (add_tfrees lmap0)
+      val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
+                 |> fold (add_thm true) cls
+                 |> add_tfrees
+                 |> fold (add_thm false) ths
       val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
       fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
       (*Now check for the existence of certain combinators*)
       val thI  = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else []
       val thK  = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else []
       val thB   = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else []
       val thC   = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
       val thS   = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
       val thEQ  = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
-      val lmap' = if mode=FO then lmap
-                  else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
+      val lmap =
+        lmap |> mode <> FO
+                ? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI)
   in
-      (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap')
+      (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap)
   end;
 
 fun refute cls =
     Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
 

 
 fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
 
 exception METIS of string;
 
-(* Main function to start metis prove and reconstruction *)
+(* Main function to start metis proof and reconstruction *)
 fun FOL_SOLVE mode ctxt cls ths0 =
   let val thy = ProofContext.theory_of ctxt
       val th_cls_pairs =
         map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
       val ths = maps #2 th_cls_pairs
       val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
       val _ = trace_msg (fn () => "THEOREM CLAUSES")
       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
-      val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
+      val (mode, {axioms, tfrees, skolem_somes}) = build_map mode ctxt cls ths
       val _ = if null tfrees then ()
               else (trace_msg (fn () => "TFREE CLAUSES");
                     app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
       val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
       val thms = map #1 axioms

             let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
                           Metis.Thm.toString mth)
                 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
                              (*add constraints arising from converting goal to clause form*)
                 val proof = Metis.Proof.proof mth
-                val result = translate mode ctxt' axioms proof
+                val result = translate ctxt' mode skolem_somes axioms proof
                 and used = map_filter (used_axioms axioms) proof
                 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
                 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
                 val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
                   if common_thm used cls then NONE else SOME name)