# HG changeset patch
# User wenzelm
# Date 1440760982 -7200
# Node ID d08a0c5a68f7840ab1b9f0f02242c0ec197f344e
# Parent  80f40d89dab609a8491047d0e19b3360d0c446d6
tuned;

diff -r 80f40d89dab6 -r d08a0c5a68f7 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Aug 28 11:53:09 2015 +0200
+++ b/src/Pure/more_thm.ML	Fri Aug 28 13:23:02 2015 +0200
@@ -196,11 +196,9 @@
 
 fun eq_thm_strict ths =
   eq_thm ths andalso
-    let val (rep1, rep2) = apply2 Thm.rep_thm ths in
-      Context.eq_thy (#thy rep1, #thy rep2) andalso
-      #maxidx rep1 = #maxidx rep2 andalso
-      #tags rep1 = #tags rep2
-    end;
+  Context.eq_thy_id (apply2 Thm.theory_id_of_thm ths) andalso
+  op = (apply2 Thm.maxidx_of ths) andalso
+  op = (apply2 Thm.get_tags ths);
 
 
 (* pattern equivalence *)