src/Pure/pure_thy.ML
changeset 17496 26535df536ae
parent 17418 cd5d8b444d6e
child 17703 6ec36bad47ea
     1.1 --- a/src/Pure/pure_thy.ML	Tue Sep 20 08:20:22 2005 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Tue Sep 20 08:21:49 2005 +0200
     1.3 @@ -250,7 +250,7 @@
     1.4    |> map (fn thy =>
     1.5        FactIndex.find (fact_index_of thy) spec
     1.6        |> List.filter (fn (name, ths) => valid_thms theory (Name name, ths))
     1.7 -      |> gen_distinct eq_fst)
     1.8 +      |> gen_distinct (eq_fst (op =)))
     1.9    |> List.concat;
    1.10  
    1.11  fun thms_containing_consts thy consts =