src/Pure/Isar/find_theorems.ML
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 =