# HG changeset patch
# User wenzelm
# Date 1204754291 -3600
# Node ID 18194535f799eac204c7ec5ea09eb067fea9562c
# Parent  499f08293680bb2132c834c8b8cf589d03d7b4cc
closeup: minor tuning of term traversal;

diff -r 499f08293680 -r 18194535f799 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Mar 05 22:48:50 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Mar 05 22:58:11 2008 +0100
@@ -1223,8 +1223,11 @@
   | closeup ctxt true elem =
       let
         fun close_frees t =
-          let val frees = rev (filter_out (Variable.is_fixed ctxt o #1) (Term.add_frees t []))
-          in Term.list_all_free (frees, t) end;
+          let
+            val rev_frees =
+              Term.fold_aterms (fn Free (x, T) =>
+                if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t [];
+          in Term.list_all_free (rev_frees, t) end;
 
         fun no_binds [] = []
           | no_binds _ = error "Illegal term bindings in locale element";