1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Jun 09 00:16:28 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Jun 09 00:16:28 2011 +0200
     1.3 @@ -34,24 +34,6 @@
     1.4  
     1.5  exception METIS of string * string
     1.6  
     1.7 -datatype term_or_type = SomeTerm of term | SomeType of typ
     1.8 -
     1.9 -fun terms_of [] = []
    1.10 -  | terms_of (SomeTerm t :: tts) = t :: terms_of tts
    1.11 -  | terms_of (SomeType _ :: tts) = terms_of tts;
    1.12 -
    1.13 -fun types_of [] = []
    1.14 -  | types_of (SomeTerm (Var ((a, idx), _)) :: tts) =
    1.15 -    types_of tts
    1.16 -    |> (if String.isPrefix metis_generated_var_prefix a then
    1.17 -          (* Variable generated by Metis, which might have been a type
    1.18 -             variable. *)
    1.19 -          cons (TVar (("'" ^ a, idx), HOLogic.typeS))
    1.20 -        else
    1.21 -          I)
    1.22 -  | types_of (SomeTerm _ :: tts) = types_of tts
    1.23 -  | types_of (SomeType T :: tts) = T :: types_of tts
    1.24 -
    1.25  fun atp_name_from_metis s =
    1.26    case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
    1.27      SOME ((s, _), (_, swap)) => (s, swap)
    1.28 @@ -188,7 +170,7 @@
    1.29  
    1.30  (* Like RSN, but we rename apart only the type variables. Vars here typically
    1.31     have an index of 1, and the use of RSN would increase this typically to 3.
    1.32 -   Instantiations of those Vars could then fail. See comment on "make_var". *)
    1.33 +   Instantiations of those Vars could then fail. *)
    1.34  fun resolve_inc_tyvars thy tha i thb =
    1.35    let
    1.36      val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha