# HG changeset patch
# User wenzelm
# Date 1438102755 -7200
# Node ID 3f38ed5a02c101e853f2f75cf05ecabaf02f4517
# Parent  92913f915e3d5237bcf3fa6d2a494d3d69ef6b22
clarified context;

diff -r 92913f915e3d -r 3f38ed5a02c1 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Jul 28 18:57:47 2015 +0200
+++ b/src/Provers/classical.ML	Tue Jul 28 18:59:15 2015 +0200
@@ -147,6 +147,7 @@
 fun classical_rule ctxt rule =
   if is_some (Object_Logic.elim_concl ctxt rule) then
     let
+      val thy = Proof_Context.theory_of ctxt;
       val rule' = rule RS Data.classical;
       val concl' = Thm.concl_of rule';
       fun redundant_hyp goal =
@@ -161,7 +162,7 @@
           else all_tac))
         |> Seq.hd
         |> Drule.zero_var_indexes;
-    in if Thm.equiv_thm (rule, rule'') then rule else rule'' end
+    in if Thm.equiv_thm thy (rule, rule'') then rule else rule'' end
   else rule;
 
 (*flatten nested meta connectives in prems*)
diff -r 92913f915e3d -r 3f38ed5a02c1 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Jul 28 18:57:47 2015 +0200
+++ b/src/Pure/more_thm.ML	Tue Jul 28 18:59:15 2015 +0200
@@ -39,7 +39,7 @@
   val eq_thm: thm * thm -> bool
   val eq_thm_prop: thm * thm -> bool
   val eq_thm_strict: thm * thm -> bool
-  val equiv_thm: thm * thm -> bool
+  val equiv_thm: theory -> thm * thm -> bool
   val class_triv: theory -> class -> thm
   val of_sort: ctyp * sort -> thm list
   val check_shyps: sort list -> thm -> thm
@@ -209,8 +209,8 @@
 
 (* pattern equivalence *)
 
-fun equiv_thm ths =
-  Pattern.equiv (Theory.merge (apply2 Thm.theory_of_thm ths)) (apply2 Thm.full_prop_of ths);
+fun equiv_thm thy ths =
+  Pattern.equiv thy (apply2 (Thm.full_prop_of o Thm.transfer thy) ths);
 
 
 (* type classes and sorts *)