src/HOL/Tools/Metis/metis_translate.ML

   val num_type_args: theory -> string -> int
   val new_skolem_var_name_from_const : string -> string
   val reveal_old_skolem_terms : (string * term) list -> term -> term
   val string_of_mode : mode -> string
   val prepare_metis_problem :
-    mode -> Proof.context -> bool -> thm list -> thm list list
-    -> mode * metis_problem
+    mode -> Proof.context -> thm list -> thm list list -> mode * metis_problem
 end
 
 structure Metis_Translate : METIS_TRANSLATE =
 struct
 

     (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 type_lits mode j old_skolems th =
+fun hol_thm_to_fol is_conjecture ctxt mode j old_skolems th =
   let
     val thy = Proof_Context.theory_of ctxt
     val (old_skolems, (mlits, types_sorts)) =
      th |> prop_of |> Logic.strip_imp_concl
         |> conceal_old_skolem_terms j old_skolems

        raw_type_literals_for_types types_sorts, old_skolems)
     else
       let
         val tylits = types_sorts |> filter_out (has_default_sort ctxt)
                                  |> raw_type_literals_for_types
-        val mtylits =
-          if type_lits then map (metis_of_type_literals false) tylits else []
+        val mtylits = map (metis_of_type_literals false) tylits
       in
         (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
          old_skolems)
       end
   end;

       val class_rel_clauses = make_class_rel_clauses thy subs supers'
   in  map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
   end;
 
 (* Function to generate metis clauses, including comb and type clauses *)
-fun prepare_metis_problem New ctxt type_lits cls thss =
+fun prepare_metis_problem New ctxt cls thss =
     error "Not implemented yet"
-  | prepare_metis_problem mode ctxt type_lits cls thss =
+  | prepare_metis_problem mode ctxt cls thss =
     let
       val thy = Proof_Context.theory_of ctxt
       (* The modes FO and FT are sticky. HO can be downgraded to FO. *)
       val mode =
         if mode = HO andalso

       (*transform isabelle clause to metis clause *)
       fun add_thm is_conjecture (isa_ith, metis_ith)
                   {axioms, tfrees, old_skolems} : metis_problem =
         let
           val (mth, tfree_lits, old_skolems) =
-            hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms)
-                           old_skolems metis_ith
+            hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems
+                           metis_ith
         in
            {axioms = (mth, isa_ith) :: axioms,
             tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
         end;
       val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}