src/Pure/Isar/find_theorems.ML

--- a/src/Pure/Isar/find_theorems.ML	Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Mon Feb 26 23:18:24 2007 +0100
@@ -227,7 +227,7 @@
   in
     map (`(eval_filters filters)) thms
     |> map_filter (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE)
-    |> sort thm_ord |> map #2 
+    |> sort thm_ord |> map #2
   end;
 
 end;
@@ -236,32 +236,30 @@
 (* removing duplicates, preferring nicer names *)
 
 fun rem_thm_dups xs =
-    let 
-      fun nicer (Fact x) (Fact y) = size x <= size y
-        | nicer (Fact _) _        = true
-        | nicer (PureThy.Name x) (PureThy.Name y) = size x <= size y
-        | nicer (PureThy.Name _) (Fact _) = false
-        | nicer (PureThy.Name _) _ = true
-        | nicer (NameSelection (x,_)) (NameSelection (y,_)) = size x <= size y
-        | nicer (NameSelection _) _ = false;
+  let
+    fun nicer (Fact x) (Fact y) = size x <= size y
+      | nicer (Fact _) _        = true
+      | nicer (PureThy.Name x) (PureThy.Name y) = size x <= size y
+      | nicer (PureThy.Name _) (Fact _) = false
+      | nicer (PureThy.Name _) _ = true
+      | nicer (NameSelection (x, _)) (NameSelection (y, _)) = size x <= size y
+      | nicer (NameSelection _) _ = false;
 
-      fun is_in [] _ = NONE
-        | is_in ((n,t) :: xs) t' = if eq_thm (t, t') 
-                                   then SOME (n,t) 
-                                   else is_in xs t';
+    fun is_in [] _ = NONE
+      | is_in ((n, t) :: xs) t' =
+          if Thm.eq_thm (t, t') then SOME (n, t) else is_in xs t';
 
-      fun eq ((_,t1),(_,t2)) = eq_thm (t1,t2)
+    fun eq ((_, t1), (_, t2)) = Thm.eq_thm (t1, t2);
 
-      fun rem_d (rev_seen, []) = rev rev_seen
-        | rem_d (rev_seen, (x as (n',t')) :: xs) = 
-          case is_in rev_seen t' of 
-            NONE => rem_d (x::rev_seen, xs)
-          | SOME (n,t) => if nicer n n' 
-                          then rem_d (rev_seen, xs) 
-                          else rem_d (x::remove eq (n,t) rev_seen,xs)
-
-    in rem_d ([], xs) end;
-
+    fun rem_d (rev_seen, []) = rev rev_seen
+      | rem_d (rev_seen, (x as (n', t')) :: xs) =
+          (case is_in rev_seen t' of
+            NONE => rem_d (x :: rev_seen, xs)
+          | SOME (n, t) =>
+              if nicer n n'
+              then rem_d (rev_seen, xs)
+              else rem_d (x :: remove eq (n, t) rev_seen, xs))
+  in rem_d ([], xs) end;
 
 
 (* print_theorems *)
@@ -272,7 +270,7 @@
   (ProofContext.lthms_containing ctxt spec
     |> maps PureThy.selections
     |> distinct (fn ((r1, th1), (r2, th2)) =>
-        r1 = r2 andalso Drule.eq_thm_prop (th1, th2)));
+        r1 = r2 andalso Thm.eq_thm_prop (th1, th2)));
 
 fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   let
@@ -280,9 +278,10 @@
     val filters = map (filter_criterion ctxt opt_goal) criteria;
 
     val raw_matches = all_filters filters (find_thms ctxt ([], []));
-    val matches = if rem_dups andalso not (null filters) 
-                  then rem_thm_dups raw_matches 
-                  else raw_matches;
+    val matches =
+      if rem_dups andalso not (null filters)
+      then rem_thm_dups raw_matches
+      else raw_matches;
 
     val len = length matches;
     val limit = the_default (! thms_containing_limit) opt_limit;