tuned;

--- 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