# 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