changeset 17496 | 26535df536ae |
parent 17451 | cfa8b1ebfc9a |
child 17756 | d4a35f82fbb4 |
--- a/src/Pure/Isar/proof_context.ML Tue Sep 20 08:20:22 2005 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Sep 20 08:21:49 2005 +0200 @@ -958,7 +958,7 @@ fun lthms_containing ctxt spec = FactIndex.find (fact_index_of ctxt) spec |> List.filter (valid_thms ctxt) - |> gen_distinct eq_fst; + |> gen_distinct (eq_fst (op =)); (* name space operations *)