src/HOL/Tools/Lifting/lifting_def.ML

         val csubst = map (pairself (cterm_of thy)) subst;
         val inst_thm = Drule.cterm_instantiate csubst thm;
       in
         Conv.fconv_rule 
           ((Conv.concl_conv (nprems_of inst_thm) o HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
-            (Raw_Simplifier.rewrite false (Transfer.get_sym_relator_eq ctxt))) inst_thm
+            (Raw_Simplifier.rewrite ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
       end
 
     fun inst_relcomppI thy ant1 ant2 =
       let
         val t1 = (HOLogic.dest_Trueprop o concl_of) ant1

     val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
     val beta_conv = Thm.beta_conversion true
     val eq_thm = 
       (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
   in
-    Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
+    Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
   end
 
 fun rename_to_tnames ctxt term =
   let
     fun all_typs (Const ("all", _) $ Abs (_, T, t)) = T :: all_typs t

           val readable_rsp_tm_tnames = rename_to_tnames lthy readable_rsp_tm
       
           fun after_qed' thm_list lthy = 
             let
               val internal_rsp_thm = Goal.prove lthy [] [] internal_rsp_tm 
-                  (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac (hd thm_list) 1)
+                  (fn {context = ctxt, ...} =>
+                    rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt (hd thm_list) 1)
             in
               after_qed internal_rsp_thm lthy
             end
         in
           Proof.theorem NONE after_qed' [[(readable_rsp_tm_tnames,[])]] lthy