changeset 19046 | bc5c6c9b114e |
parent 18939 | 18e2a2676d80 |
child 19476 | 816f519f8b72 |
--- a/src/Pure/Isar/find_theorems.ML Wed Feb 15 19:11:10 2006 +0100 +++ b/src/Pure/Isar/find_theorems.ML Wed Feb 15 21:34:55 2006 +0100 @@ -242,7 +242,7 @@ (ProofContext.lthms_containing ctxt spec |> map PureThy.selections |> List.concat - |> gen_distinct (fn ((r1, th1), (r2, th2)) => + |> 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 =