# HG changeset patch
# User wenzelm
# Date 1393085610 -3600
# Node ID 95454b2980ee4053813a5a3937da62f309bdc448
# Parent  4612c450b59c1d3609c854dfbde96f4cf848b17b
removed dead code;
more complete patterns;

diff -r 4612c450b59c -r 95454b2980ee src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat Feb 22 16:58:02 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sat Feb 22 17:13:30 2014 +0100
@@ -96,12 +96,6 @@
   Internal of Facts.ref * thm |
   External of Facts.ref * term; (* FIXME: Facts.ref not appropriate *)
 
-fun fact_ref_markup (Facts.Named ((name, pos), SOME [Facts.Single i])) =
-      Position.markup pos o Markup.properties [("name", name), ("index", Markup.print_int i)]
-  | fact_ref_markup (Facts.Named ((name, pos), NONE)) =
-      Position.markup pos o Markup.properties [("name", name)]
-  | fact_ref_markup fact_ref = raise Fail "bad fact ref";
-
 fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
   | prop_of (External (_, prop)) = prop;
 
@@ -375,9 +369,9 @@
     fun rem_c rev_seen [] = rev rev_seen
       | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
       | rem_c rev_seen ((x as (t, _)) :: (y as (t', _)) :: xs) =
-          if (prop_of t) aconv (prop_of t')
+          if prop_of t aconv prop_of t'
           then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs)
-          else rem_c (x :: rev_seen) (y :: xs)
+          else rem_c (x :: rev_seen) (y :: xs);
   in rem_c [] xs end;
 
 in
@@ -396,7 +390,8 @@
     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
           nicer_name (shorten x, i) (shorten y, j)
       | nicer (Facts.Fact _) (Facts.Named _) = true
-      | nicer (Facts.Named _) (Facts.Fact _) = false;
+      | nicer (Facts.Named _) (Facts.Fact _) = false
+      | nicer (Facts.Fact _) (Facts.Fact _) = true;
   in nicer end;
 
 fun rem_thm_dups nicer xs =