--- 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