1.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Wed Dec 31 00:08:11 2008 +0100
     1.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Wed Dec 31 00:08:13 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Tools/IsaPlanner/rw_inst.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Lucas Dixon, University of Edinburgh
     1.7  
     1.8  Rewriting using a conditional meta-equality theorem which supports
     1.9 @@ -143,9 +142,9 @@
    1.10                      (Library.union
    1.11                         (Term.term_tvars t, tyvs),
    1.12                       Library.union 
    1.13 -                       (map Term.dest_Var (Term.term_vars t), vs))) 
    1.14 +                       (map Term.dest_Var (OldTerm.term_vars t), vs))) 
    1.15                  (([],[]), rule_conds);
    1.16 -      val termvars = map Term.dest_Var (Term.term_vars tgt); 
    1.17 +      val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
    1.18        val vars_to_fix = Library.union (termvars, cond_vs);
    1.19        val (renamings, names2) = 
    1.20            foldr (fn (((n,i),ty), (vs, names')) =>