--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Jun 09 00:16:28 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Jun 09 00:16:28 2011 +0200
@@ -34,24 +34,6 @@
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)
@@ -188,7 +170,7 @@
(* 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