# HG changeset patch
# User wenzelm
# Date 1230749644 -3600
# Node ID 7456a64bc4f68bbfafcfccd57a756ffbe825d5cf
# Parent  e9d148a808eb4c42371ed6f44bce5f9fe4baaeb0
Term.declare_typ_names, Term.declare_term_frees;

diff -r e9d148a808eb -r 7456a64bc4f6 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Dec 31 19:54:04 2008 +0100
+++ b/src/Pure/variable.ML	Wed Dec 31 19:54:04 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/variable.ML
-    ID:         $Id$
     Author:     Makarius
 
 Fixed type/term variables and polymorphic term abbreviations.
@@ -179,12 +178,12 @@
 (* names *)
 
 fun declare_type_names t =
-  map_names (fold_types (fold_atyps (fn TFree (a, _) => Name.declare a | _ => I)) t) #>
+  map_names (fold_types (fold_atyps Term.declare_typ_names) t) #>
   map_maxidx (fold_types Term.maxidx_typ t);
 
 fun declare_names t =
   declare_type_names t #>
-  map_names (fold_aterms (fn Free (x, _) => Name.declare x | _ => I) t) #>
+  map_names (fold_aterms Term.declare_term_frees t) #>
   map_maxidx (Term.maxidx_term t);