src/HOL/Tools/Sledgehammer/metis_tactics.ML

-(*  Title:      HOL/Tools/metis_tools.ML
+(*  Title:      HOL/Tools/Sledgehammer/metis_tactics.ML
     Author:     Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory
     Copyright   Cambridge University 2007
 
 HOL setup for the Metis prover.
 *)
 
-signature METIS_TOOLS =
+signature METIS_TACTICS =
 sig
   val trace: bool Unsynchronized.ref
   val type_lits: bool Config.T
   val metis_tac: Proof.context -> thm list -> int -> tactic
   val metisF_tac: Proof.context -> thm list -> int -> tactic
   val metisFT_tac: Proof.context -> thm list -> int -> tactic
   val setup: theory -> theory
 end
 
-structure MetisTools: METIS_TOOLS =
+structure Metis_Tactics : METIS_TACTICS =
 struct
 
+structure SFC = Sledgehammer_FOL_Clause
+structure SHC = Sledgehammer_HOL_Clause
+structure SPR = Sledgehammer_Proof_Reconstruct
+
 val trace = Unsynchronized.ref false;
-fun trace_msg msg = if ! trace then tracing (msg ()) else ();
+fun trace_msg msg = if !trace then tracing (msg ()) else ();
 
 val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
 
-datatype mode = FO | HO | FT  (*first-order, higher-order, fully-typed*)
+datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
 
 (* ------------------------------------------------------------------------- *)
 (* Useful Theorems                                                           *)
 (* ------------------------------------------------------------------------- *)
 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}

 fun fn_isa_to_met "equal" = "="
   | fn_isa_to_met x       = x;
 
 fun metis_lit b c args = (b, (c, args));
 
-fun hol_type_to_fol (Res_Clause.AtomV x) = Metis.Term.Var x
-  | hol_type_to_fol (Res_Clause.AtomF x) = Metis.Term.Fn(x,[])
-  | hol_type_to_fol (Res_Clause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
+fun hol_type_to_fol (SFC.AtomV x) = Metis.Term.Var x
+  | hol_type_to_fol (SFC.AtomF x) = Metis.Term.Fn(x,[])
+  | hol_type_to_fol (SFC.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
 
 (*These two functions insert type literals before the real literals. That is the
   opposite order from TPTP linkup, but maybe OK.*)
 
 fun hol_term_to_fol_FO tm =
-  case Res_HOL_Clause.strip_comb tm of
-      (Res_HOL_Clause.CombConst(c,_,tys), tms) =>
+  case SHC.strip_comb tm of
+      (SHC.CombConst(c,_,tys), tms) =>
         let val tyargs = map hol_type_to_fol tys
             val args   = map hol_term_to_fol_FO tms
         in Metis.Term.Fn (c, tyargs @ args) end
-    | (Res_HOL_Clause.CombVar(v,_), []) => Metis.Term.Var v
+    | (SHC.CombVar(v,_), []) => Metis.Term.Var v
     | _ => error "hol_term_to_fol_FO";
 
-fun hol_term_to_fol_HO (Res_HOL_Clause.CombVar (a, _)) = Metis.Term.Var a
-  | hol_term_to_fol_HO (Res_HOL_Clause.CombConst (a, _, tylist)) =
+fun hol_term_to_fol_HO (SHC.CombVar (a, _)) = Metis.Term.Var a
+  | hol_term_to_fol_HO (SHC.CombConst (a, _, tylist)) =
       Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
-  | hol_term_to_fol_HO (Res_HOL_Clause.CombApp (tm1, tm2)) =
+  | hol_term_to_fol_HO (SHC.CombApp (tm1, tm2)) =
        Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
 
 (*The fully-typed translation, to avoid type errors*)
 fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
 
-fun hol_term_to_fol_FT (Res_HOL_Clause.CombVar(a, ty)) =
+fun hol_term_to_fol_FT (SHC.CombVar(a, ty)) =
       wrap_type (Metis.Term.Var a, ty)
-  | hol_term_to_fol_FT (Res_HOL_Clause.CombConst(a, ty, _)) =
+  | hol_term_to_fol_FT (SHC.CombConst(a, ty, _)) =
       wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
-  | hol_term_to_fol_FT (tm as Res_HOL_Clause.CombApp(tm1,tm2)) =
+  | hol_term_to_fol_FT (tm as SHC.CombApp(tm1,tm2)) =
        wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
-                  Res_HOL_Clause.type_of_combterm tm);
-
-fun hol_literal_to_fol FO (Res_HOL_Clause.Literal (pol, tm)) =
-      let val (Res_HOL_Clause.CombConst(p,_,tys), tms) = Res_HOL_Clause.strip_comb tm
+                  SHC.type_of_combterm tm);
+
+fun hol_literal_to_fol FO (SHC.Literal (pol, tm)) =
+      let val (SHC.CombConst(p,_,tys), tms) = SHC.strip_comb tm
           val tylits = if p = "equal" then [] else map hol_type_to_fol tys
           val lits = map hol_term_to_fol_FO tms
       in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
-  | hol_literal_to_fol HO (Res_HOL_Clause.Literal (pol, tm)) =
-     (case Res_HOL_Clause.strip_comb tm of
-          (Res_HOL_Clause.CombConst("equal",_,_), tms) =>
+  | hol_literal_to_fol HO (SHC.Literal (pol, tm)) =
+     (case SHC.strip_comb tm of
+          (SHC.CombConst("equal",_,_), tms) =>
             metis_lit pol "=" (map hol_term_to_fol_HO tms)
         | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
-  | hol_literal_to_fol FT (Res_HOL_Clause.Literal (pol, tm)) =
-     (case Res_HOL_Clause.strip_comb tm of
-          (Res_HOL_Clause.CombConst("equal",_,_), tms) =>
+  | hol_literal_to_fol FT (SHC.Literal (pol, tm)) =
+     (case SHC.strip_comb tm of
+          (SHC.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 =
-      let val (lits, types_sorts) = Res_HOL_Clause.literals_of_term thy t
+      let val (lits, types_sorts) = SHC.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_typeLit pos (Res_Clause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
-  | metis_of_typeLit pos (Res_Clause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
+fun metis_of_typeLit pos (SFC.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
+  | metis_of_typeLit pos (SFC.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
 
 fun default_sort _ (TVar _) = false
   | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
 
 fun metis_of_tfree tf =

   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
   in
       if is_conjecture then
-          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), Res_Clause.add_typs types_sorts)
+          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), SFC.add_typs types_sorts)
       else
-        let val tylits = Res_Clause.add_typs
+        let val tylits = SFC.add_typs
                            (filter (not o default_sort ctxt) types_sorts)
             val mtylits = if Config.get ctxt type_lits
                           then map (metis_of_typeLit false) tylits else []
         in
           (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
         end
   end;
 
 (* ARITY CLAUSE *)
 
-fun m_arity_cls (Res_Clause.TConsLit (c,t,args)) =
-      metis_lit true (Res_Clause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
-  | m_arity_cls (Res_Clause.TVarLit (c,str))     =
-      metis_lit false (Res_Clause.make_type_class c) [Metis.Term.Var str];
+fun m_arity_cls (SFC.TConsLit (c,t,args)) =
+      metis_lit true (SFC.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
+  | m_arity_cls (SFC.TVarLit (c,str))     =
+      metis_lit false (SFC.make_type_class c) [Metis.Term.Var str];
 
 (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
-fun arity_cls (Res_Clause.ArityClause{conclLit,premLits,...}) =
+fun arity_cls (SFC.ArityClause{conclLit,premLits,...}) =
   (TrueI,
    Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
 
 (* CLASSREL CLAUSE *)
 
 fun m_classrel_cls subclass superclass =
   [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
 
-fun classrel_cls (Res_Clause.ClassrelClause {subclass, superclass, ...}) =
+fun classrel_cls (SFC.ClassrelClause {subclass, superclass, ...}) =
   (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
 
 (* ------------------------------------------------------------------------- *)
 (* FOL to HOL  (Metis to Isabelle)                                           *)
 (* ------------------------------------------------------------------------- *)

 (*Remove the "apply" operator from an HO term*)
 fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
   | strip_happ args x = (x, args);
 
 fun fol_type_to_isa _ (Metis.Term.Var v) =
-     (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of
-          SOME w => Res_Reconstruct.make_tvar w
-        | NONE   => Res_Reconstruct.make_tvar v)
+     (case SPR.strip_prefix SFC.tvar_prefix v of
+          SOME w => SPR.make_tvar w
+        | NONE   => SPR.make_tvar v)
   | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
-     (case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix x of
-          SOME tc => Term.Type (Res_Reconstruct.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
+     (case SPR.strip_prefix SFC.tconst_prefix x of
+          SOME tc => Term.Type (SPR.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
         | NONE    =>
-      case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix x of
+      case SPR.strip_prefix SFC.tfree_prefix x of
           SOME tf => mk_tfree ctxt tf
         | NONE    => error ("fol_type_to_isa: " ^ x));
 
 (*Maps metis terms to isabelle terms*)
 fun fol_term_to_hol_RAW ctxt fol_tm =
   let val thy = ProofContext.theory_of ctxt
       val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
       fun tm_to_tt (Metis.Term.Var v) =
-             (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of
-                  SOME w => Type (Res_Reconstruct.make_tvar w)
+             (case SPR.strip_prefix SFC.tvar_prefix v of
+                  SOME w => Type (SPR.make_tvar w)
                 | NONE =>
-              case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of
+              case SPR.strip_prefix SFC.schematic_var_prefix v of
                   SOME w => Term (mk_var (w, HOLogic.typeT))
                 | NONE   => Term (mk_var (v, HOLogic.typeT)) )
                     (*Var from Metis with a name like _nnn; possibly a type variable*)
         | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
         | tm_to_tt (t as Metis.Term.Fn (".",_)) =

             end
         | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
       and applic_to_tt ("=",ts) =
             Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
         | applic_to_tt (a,ts) =
-            case Res_Reconstruct.strip_prefix Res_Clause.const_prefix a of
+            case SPR.strip_prefix SFC.const_prefix a of
                 SOME b =>
-                  let val c = Res_Reconstruct.invert_const b
-                      val ntypes = Res_Reconstruct.num_typargs thy c
+                  let val c = SPR.invert_const b
+                      val ntypes = SPR.num_typargs thy c
                       val nterms = length ts - ntypes
                       val tts = map tm_to_tt ts
                       val tys = types_of (List.take(tts,ntypes))
-                      val ntyargs = Res_Reconstruct.num_typargs thy c
+                      val ntyargs = SPR.num_typargs thy c
                   in if length tys = ntyargs then
                          apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
                      else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
                                  " but gets " ^ Int.toString (length tys) ^
                                  " type arguments\n" ^
                                  cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
                                  " the terms are \n" ^
                                  cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
                      end
               | NONE => (*Not a constant. Is it a type constructor?*)
-            case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix a of
+            case SPR.strip_prefix SFC.tconst_prefix a of
                 SOME b =>
-                  Type (Term.Type (Res_Reconstruct.invert_type_const b, types_of (map tm_to_tt ts)))
+                  Type (Term.Type (SPR.invert_type_const b, types_of (map tm_to_tt ts)))
               | NONE => (*Maybe a TFree. Should then check that ts=[].*)
-            case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix a of
+            case SPR.strip_prefix SFC.tfree_prefix a of
                 SOME b => Type (mk_tfree ctxt b)
               | NONE => (*a fixed variable? They are Skolem functions.*)
-            case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix a of
+            case SPR.strip_prefix SFC.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;
 
 (*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 cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
-             (case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of
+             (case SPR.strip_prefix SFC.schematic_var_prefix v of
                   SOME w =>  mk_var(w, dummyT)
                 | NONE   => mk_var(v, dummyT))
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
             Const ("op =", HOLogic.typeT)
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
-           (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of
-                SOME c => Const (Res_Reconstruct.invert_const c, dummyT)
+           (case SPR.strip_prefix SFC.const_prefix x of
+                SOME c => Const (SPR.invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
-            case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of
+            case SPR.strip_prefix SFC.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))
         | 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*)
         | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
             list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
         | cvt (t as Metis.Term.Fn (x, [])) =
-           (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of
-                SOME c => Const (Res_Reconstruct.invert_const c, dummyT)
+           (case SPR.strip_prefix SFC.const_prefix x of
+                SOME c => Const (SPR.invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
-            case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of
+            case SPR.strip_prefix SFC.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)

             handle Option =>
                 (trace_msg (fn() => "List.find failed for the variable " ^ x ^
                                        " in " ^ Display.string_of_thm ctxt i_th);
                  NONE)
       fun remove_typeinst (a, t) =
-            case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix a of
+            case SPR.strip_prefix SFC.schematic_var_prefix a of
                 SOME b => SOME (b, t)
-              | NONE   => case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix a of
+              | NONE   => case SPR.strip_prefix SFC.tvar_prefix a of
                 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 _ = 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 ("op =", _)) = 0  (*equality has no type arguments*)
-  | get_ty_arg_size thy (Const (c, _)) = (Res_Reconstruct.num_typargs thy c handle TYPE _ => 0)
+  | get_ty_arg_size thy (Const (c, _)) = (SPR.num_typargs thy c handle TYPE _ => 0)
   | get_ty_arg_size _ _ = 0;
 
 (* INFERENCE RULE: EQUALITY *)
 fun equality_inf ctxt mode (pos, atm) fp fr =
   let val thy = ProofContext.theory_of ctxt

       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 real_literal (_, (c, _)) = not (String.isPrefix Res_Clause.class_prefix c);
+fun real_literal (_, (c, _)) = not (String.isPrefix SFC.class_prefix c);
 
 fun translate _ _ thpairs [] = thpairs
   | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
       let val _ = trace_msg (fn () => "=============================================")
           val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)

 
 (* ------------------------------------------------------------------------- *)
 (* Translation of HO Clauses                                                 *)
 (* ------------------------------------------------------------------------- *)
 
-fun cnf_th thy th = hd (Res_Axioms.cnf_axiom thy th);
+fun cnf_th thy th = hd (Sledgehammer_Fact_Preprocessor.cnf_axiom thy th);
 
 val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
 val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
 
-val comb_I = cnf_th @{theory} Res_HOL_Clause.comb_I;
-val comb_K = cnf_th @{theory} Res_HOL_Clause.comb_K;
-val comb_B = cnf_th @{theory} Res_HOL_Clause.comb_B;
-val comb_C = cnf_th @{theory} Res_HOL_Clause.comb_C;
-val comb_S = cnf_th @{theory} Res_HOL_Clause.comb_S;
+val comb_I = cnf_th @{theory} SHC.comb_I;
+val comb_K = cnf_th @{theory} SHC.comb_K;
+val comb_B = cnf_th @{theory} SHC.comb_B;
+val comb_C = cnf_th @{theory} SHC.comb_C;
+val comb_S = cnf_th @{theory} SHC.comb_S;
 
 fun type_ext thy tms =
-  let val subs = Res_ATP.tfree_classes_of_terms tms
-      val supers = Res_ATP.tvar_classes_of_terms tms
-      and tycons = Res_ATP.type_consts_of_terms thy tms
-      val (supers', arity_clauses) = Res_Clause.make_arity_clauses thy tycons supers
-      val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers'
+  let val subs = Sledgehammer_Fact_Filter.tfree_classes_of_terms tms
+      val supers = Sledgehammer_Fact_Filter.tvar_classes_of_terms tms
+      and tycons = Sledgehammer_Fact_Filter.type_consts_of_terms thy tms
+      val (supers', arity_clauses) = SFC.make_arity_clauses thy tycons supers
+      val classrel_clauses = SFC.make_classrel_clauses thy subs supers'
   in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
   end;
 
 (* ------------------------------------------------------------------------- *)
 (* Logic maps manage the interface between HOL and first-order logic.        *)
 (* ------------------------------------------------------------------------- *)
 
 type logic_map =
   {axioms : (Metis.Thm.thm * thm) list,
-   tfrees : Res_Clause.type_literal list};
+   tfrees : SFC.type_literal 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

   in  c = pred orelse exists in_mterm tm_list  end;
 
 (*Extract TFree constraints from context to include as conjecture clauses*)
 fun init_tfrees ctxt =
   let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
-  in  Res_Clause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
+  in  SFC.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) 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,

 exception METIS of string;
 
 (* Main function to start metis prove 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, Res_Axioms.cnf_axiom thy th)) ths0
+      val th_cls_pairs =
+        map (fn th => (Thm.get_name_hint th, Sledgehammer_Fact_Preprocessor.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 _ = if null tfrees then ()
               else (trace_msg (fn () => "TFREE CLAUSES");
-                    app (fn tf => trace_msg (fn _ => Res_Clause.tptp_of_typeLit true tf)) tfrees)
+                    app (fn tf => trace_msg (fn _ => SFC.tptp_of_typeLit true tf)) tfrees)
       val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
       val thms = map #1 axioms
       val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
       val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
       val _ = trace_msg (fn () => "START METIS PROVE PROCESS")

 
 fun metis_general_tac mode ctxt ths i st0 =
   let val _ = trace_msg (fn () =>
         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   in
-    if exists_type Res_Axioms.type_has_topsort (prop_of st0)
+    if exists_type Sledgehammer_Fact_Preprocessor.type_has_topsort (prop_of st0)
     then raise METIS "Metis: Proof state contains the universal sort {}"
     else
-      (Meson.MESON Res_Axioms.neg_clausify
+      (Meson.MESON Sledgehammer_Fact_Preprocessor.neg_clausify
         (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
-          THEN Res_Axioms.expand_defs_tac st0) st0
+          THEN Sledgehammer_Fact_Preprocessor.expand_defs_tac st0) st0
   end
   handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
 
 val metis_tac = metis_general_tac HO;
 val metisF_tac = metis_general_tac FO;

   type_lits_setup #>
   method @{binding metis} HO "METIS for FOL & HOL problems" #>
   method @{binding metisF} FO "METIS for FOL problems" #>
   method @{binding metisFT} FT "METIS with fully-typed translation" #>
   Method.setup @{binding finish_clausify}
-    (Scan.succeed (K (SIMPLE_METHOD (Res_Axioms.expand_defs_tac refl))))
+    (Scan.succeed (K (SIMPLE_METHOD (Sledgehammer_Fact_Preprocessor.expand_defs_tac refl))))
     "cleanup after conversion to clauses";
 
 end;