ProofContext.lthms_containing: suppress obvious duplicates;
authorwenzelm
Thu Dec 01 22:03:04 2005 +0100 (2005-12-01)
changeset 183252d504ea54e5b
parent 18324 d1c4b1112e33
child 18326 2f57579e618f
ProofContext.lthms_containing: suppress obvious duplicates;
src/Pure/Isar/find_theorems.ML
     1.1 --- a/src/Pure/Isar/find_theorems.ML	Thu Dec 01 22:03:01 2005 +0100
     1.2 +++ b/src/Pure/Isar/find_theorems.ML	Thu Dec 01 22:03:04 2005 +0100
     1.3 @@ -236,9 +236,14 @@
     1.4  (* print_theorems *)
     1.5  
     1.6  fun find_thms ctxt spec =
     1.7 -  (PureThy.thms_containing (ProofContext.theory_of ctxt) spec @
     1.8 -    ProofContext.lthms_containing ctxt spec)
     1.9 -  |> map PureThy.selections |> List.concat;
    1.10 +  (PureThy.thms_containing (ProofContext.theory_of ctxt) spec
    1.11 +    |> map PureThy.selections
    1.12 +    |> List.concat) @
    1.13 +  (ProofContext.lthms_containing ctxt spec
    1.14 +    |> map PureThy.selections
    1.15 +    |> List.concat
    1.16 +    |> gen_distinct (fn ((r1, th1), (r2, th2)) =>
    1.17 +        r1 = r2 andalso Drule.eq_thm_prop (th1, th2)));
    1.18  
    1.19  fun print_theorems ctxt opt_goal opt_limit raw_criteria =
    1.20    let