# HG changeset patch
# User wenzelm
# Date 1133470984 -3600
# Node ID 2d504ea54e5b4a14d8fde233d18eb17cbbdd9d1e
# Parent  d1c4b1112e33778383c096bcfabf57e10a59e9cf
ProofContext.lthms_containing: suppress obvious duplicates;

diff -r d1c4b1112e33 -r 2d504ea54e5b src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Thu Dec 01 22:03:01 2005 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Thu Dec 01 22:03:04 2005 +0100
@@ -236,9 +236,14 @@
 (* print_theorems *)
 
 fun find_thms ctxt spec =
-  (PureThy.thms_containing (ProofContext.theory_of ctxt) spec @
-    ProofContext.lthms_containing ctxt spec)
-  |> map PureThy.selections |> List.concat;
+  (PureThy.thms_containing (ProofContext.theory_of ctxt) spec
+    |> map PureThy.selections
+    |> List.concat) @
+  (ProofContext.lthms_containing ctxt spec
+    |> map PureThy.selections
+    |> List.concat
+    |> gen_distinct (fn ((r1, th1), (r2, th2)) =>
+        r1 = r2 andalso Drule.eq_thm_prop (th1, th2)));
 
 fun print_theorems ctxt opt_goal opt_limit raw_criteria =
   let