--- 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 *)