# HG changeset patch
# User wenzelm
# Date 1121259360 -7200
# Node ID 51600bfac17680d708183217295ae95783a31872
# Parent  e6ba3819e4048e27666d1d5079d4eb0c09d29022
fixed comment-out;

diff -r e6ba3819e404 -r 51600bfac176 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Jul 13 12:24:39 2005 +0200
+++ b/src/Pure/term.ML	Wed Jul 13 14:56:00 2005 +0200
@@ -1246,7 +1246,7 @@
 val add_frees =
   let fun add_frees' (Free v) = insert (op =) v
          | add_frees' _ = I
-  in uncurry (fold_aterms add_frees') o swap end;*)
+  in uncurry (fold_aterms add_frees') o swap end;
 
 (*collect variable names*)
 val add_term_varnames =