# HG changeset patch
# User wenzelm
# Date 1206475261 -3600
# Node ID 9e0e4ce5131362d217d5221b6cb0d2e4c0f1bdc3
# Parent  ddd7825ea4cd6008fb2aca40d1d1758a8e2a29ad
get fact: do not compare names;

diff -r ddd7825ea4cd -r 9e0e4ce51313 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Mar 25 21:01:00 2008 +0100
+++ b/src/Pure/pure_thy.ML	Tue Mar 25 21:01:01 2008 +0100
@@ -195,7 +195,7 @@
     val is_same =
       (case (new_res, old_res) of
         (NONE, NONE) => true
-      | (SOME (name1, ths1), SOME (name2, ths2)) => name1 = name2 andalso Thm.eq_thms (ths1, ths2)
+      | (SOME (_, ths1), SOME (_, ths2)) => Thm.eq_thms (ths1, ths2)
       | _ => false);
     val _ =
       if is_same orelse silent then ()