# HG changeset patch
# User wenzelm
# Date 1312998357 -7200
# Node ID 69e29cf993c008b43182464d83ce1ad7eed14184
# Parent  88a5a8f44d1513b9c61e0f26eb68dfe08f1b4897
avoid OldTerm operations -- with subtle changes of semantics;

diff -r 88a5a8f44d15 -r 69e29cf993c0 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Aug 10 19:45:41 2011 +0200
+++ b/src/Pure/proofterm.ML	Wed Aug 10 19:45:57 2011 +0200
@@ -461,15 +461,15 @@
 fun del_conflicting_tvars envT T = Term_Subst.instantiateT
   (map_filter (fn ixnS as (_, S) =>
      (Type.lookup envT ixnS; NONE) handle TYPE _ =>
-        SOME (ixnS, TFree ("'dummy", S))) (OldTerm.typ_tvars T)) T;
+        SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvarsT T [])) T;
 
 fun del_conflicting_vars env t = Term_Subst.instantiate
   (map_filter (fn ixnS as (_, S) =>
      (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
-        SOME (ixnS, TFree ("'dummy", S))) (OldTerm.term_tvars t),
-   map_filter (fn Var (ixnT as (_, T)) =>
+        SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvars t []),
+   map_filter (fn (ixnT as (_, T)) =>
      (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
-        SOME (ixnT, Free ("dummy", T))) (OldTerm.term_vars t)) t;
+        SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t;
 
 fun norm_proof env =
   let