| changeset 19046 | bc5c6c9b114e |
| parent 18838 | d32f70789342 |
| child 19125 | 59b26248547b |
--- a/src/Pure/pure_thy.ML Wed Feb 15 19:11:10 2006 +0100 +++ b/src/Pure/pure_thy.ML Wed Feb 15 21:34:55 2006 +0100 @@ -312,7 +312,7 @@ |> map (fn thy => FactIndex.find (fact_index_of thy) spec |> List.filter (fn (name, ths) => valid_thms theory (Name name, ths)) - |> gen_distinct (eq_fst (op =))) + |> distinct (eq_fst (op =))) |> List.concat; fun thms_containing_consts thy consts =