# HG changeset patch
# User clasohm
# Date 790860010 -3600
# Node ID 1c060d444a810994307b509c5329628cb71d79ce
# Parent  ef6faaa415dc9a701f5fcf53663a16de0dfdf80e
simplified get_thm a bit

diff -r ef6faaa415dc -r 1c060d444a81 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Fri Jan 20 10:41:01 1995 +0100
+++ b/src/Pure/Thy/thy_read.ML	Mon Jan 23 12:20:10 1995 +0100
@@ -538,11 +538,11 @@
   let fun get [] [] searched =
            raise THEORY ("get_thm: no theorem " ^ quote name, [thy])
         | get [] ng searched =
-            get (distinct (gen_rems (op =) (ng, searched))) [] searched
+            get (ng \\ searched) [] searched
         | get (t::ts) ng searched =
             (case Symtab.lookup (thmtab_ofname t, name) of
                  Some thm => thm
-               | None => get ts (ng @ get_parents t) (t::searched));
+               | None => get ts (ng union (get_parents t)) (t::searched));
 
       val (tname, _) = thyinfo_of_sign (sign_of thy);
   in get [tname] [] [] end;