src/Provers/classical.ML

 *)
 
 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 =
         concl' aconv Logic.strip_assums_concl goal orelse
           (case Logic.strip_assums_hyp goal of

           if i = 1 orelse redundant_hyp goal
           then eresolve_tac ctxt [thin_rl] i
           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*)
 fun flat_rule ctxt =
   Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt));