# HG changeset patch
# User blanchet
# Date 1307571388 -7200
# Node ID 854f667df3d64ba72a4c67c19d501c0d29bbaecd
# Parent  f78d5f0818a0f8d738ce97dd7fe4e7291b150784
removed more dead code

diff -r f78d5f0818a0 -r 854f667df3d6 src/HOL/Tools/Metis/metis_reconstruct.ML
--- 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