changeset 20664 | ffbc5a57191a |
parent 20548 | 8ef25fe585a8 |
child 20872 | 528054ca23e3 |
--- a/src/Pure/Isar/locale.ML Thu Sep 21 19:04:12 2006 +0200 +++ b/src/Pure/Isar/locale.ML Thu Sep 21 19:04:20 2006 +0200 @@ -1644,7 +1644,7 @@ val (body, bodyT, body_eq) = atomize_spec thy norm_ts; val env = Term.add_term_free_names (body, []); - val xs = filter (fn (x, _) => x mem_string env) parms; + val xs = filter (member (op =) env o #1) parms; val Ts = map #2 xs; val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts) |> Library.sort_wrt #1 |> map TFree;