src/HOL/Tools/Metis/metis_reconstruct.ML

 open ATP_Translate
 open ATP_Reconstruct
 open Metis_Translate
 
 exception METIS of string * string
-
-datatype term_or_type = SomeTerm of term | SomeType of typ
-
-fun terms_of [] = []
-  | terms_of (SomeTerm t :: tts) = t :: terms_of tts
-  | terms_of (SomeType _ :: tts) = terms_of tts;
-
-fun types_of [] = []
-  | types_of (SomeTerm (Var ((a, idx), _)) :: tts) =
-    types_of tts
-    |> (if String.isPrefix metis_generated_var_prefix a then
-          (* Variable generated by Metis, which might have been a type
-             variable. *)
-          cons (TVar (("'" ^ a, idx), HOLogic.typeS))
-        else
-          I)
-  | types_of (SomeTerm _ :: tts) = types_of tts
-  | types_of (SomeType T :: tts) = T :: types_of tts
 
 fun atp_name_from_metis s =
   case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
     SOME ((s, _), (_, swap)) => (s, swap)
   | _ => (s, false)

 
 (* 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 could then fail. See comment on "make_var". *)
+   Instantiations of those Vars could then fail. *)
 fun resolve_inc_tyvars thy tha i thb =
   let
     val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
     fun aux tha thb =
       case Thm.bicompose false (false, tha, nprems_of tha) i thb