src/Pure/pure_thy.ML
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 =