# HG changeset patch
# User wenzelm
# Date 1008944287 -3600
# Node ID f4e0ce28aa8e598e84e3cb3eb1da116579216387
# Parent  c76c4b88ca6aeb8f6e3710e4043e0f85a687207a
tuned;

diff -r c76c4b88ca6a -r f4e0ce28aa8e src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Dec 21 00:44:35 2001 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Dec 21 15:18:07 2001 +0100
@@ -215,8 +215,8 @@
         val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th;
         val cert = Thm.cterm_of sign;
         val certT = Thm.ctyp_of sign;
-        val occs = foldr Term.add_term_tfree_names (prop :: hyps, []);
-        val env' = filter (fn ((a, _), _) => a mem_string occs) env;
+        val tfrees = foldr Term.add_term_tfree_names (prop :: hyps, []);
+        val env' = filter (fn ((a, _), _) => a mem_string tfrees) env;
       in
         if null env' then th
         else