src/HOL/Tools/Lifting/lifting_def_code_dt.ML

 
     val unfold_lift_sel_rsp = @{lemma "(\<And>x. P1 x \<Longrightarrow> P2 (f x)) \<Longrightarrow> (rel_fun (eq_onp P1) (eq_onp P2)) f f"
       by (simp add: eq_onp_same_args rel_fun_eq_onp_rel)}
 
     fun lift_sel_tac exhaust_rule dt_rules wits ctxt i =
-        (Method.insert_tac wits THEN' 
+        (Method.insert_tac ctxt wits THEN' 
          eq_onp_to_top_tac ctxt THEN' (* normalize *)
          rtac ctxt unfold_lift_sel_rsp THEN'
          case_tac exhaust_rule ctxt THEN_ALL_NEW (
         EVERY' [hyp_subst_tac ctxt, (* does not kill wits because = was rewritten to eq_onp top *)
         Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules), 

         val pred = quot_thm_rel quot_thm |> dest_comb |> snd;
         val (pred, lthy) = yield_singleton (Variable.import_terms true) pred lthy;
         val TFrees = Term.add_tfreesT qty []
 
         fun non_empty_typedef_tac non_empty_pred ctxt i =
-          (Method.insert_tac [non_empty_pred] THEN' 
+          (Method.insert_tac ctxt [non_empty_pred] THEN' 
             SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' assume_tac ctxt) i
         val uTname = unique_Tname (rty, qty)
         val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
         val ((_, tcode_dt), lthy) = conceal_naming_result (typedef (Binding.concealed uTname, TFrees, NoSyn)
           Tdef_set NONE (fn lthy => HEADGOAL (non_empty_typedef_tac non_empty_pred lthy))) lthy;