1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 10 20:12:36 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 10 20:53:43 2011 +0200
     1.3 @@ -372,7 +372,7 @@
     1.4        val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
     1.5        val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
     1.6        val eq_terms = map (pairself (cterm_of thy))
     1.7 -        (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
     1.8 +        (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
     1.9    in  cterm_instantiate eq_terms subst'  end;
    1.10  
    1.11  val factor = Seq.hd o distinct_subgoals_tac