# 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