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