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