src/HOL/Decision_Procs/mir_tac.ML

         THEN' simp_tac (put_simpset HOL_basic_ss ctxt
           addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms})
         THEN' (REPEAT_DETERM o split_tac ctxt [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
         THEN' SUBGOAL (fn (g, i) =>
   let
-    val thy = Proof_Context.theory_of ctxt
     (* Transform the term*)
     val (t,np,nh) = prepare_for_mir q g
     (* Some simpsets for dealing with mod div abs and nat*)
     val mod_div_simpset = put_simpset HOL_basic_ss ctxt
                         addsimps [refl, mod_add_eq, 

     val simpset2 = put_simpset HOL_basic_ss ctxt
       addsimps [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm zero_le_numeral}, 
                 @{thm "int_0"}, @{thm "int_1"}]
       |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
     (* simp rules for elimination of abs *)
-    val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
+    val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
     (* Theorem for the nat --> int transformation *)
     val pre_thm = Seq.hd (EVERY
       [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
        TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
        TRY (simp_tac (put_simpset mir_ss ctxt) 1)]

       case Thm.prop_of pre_thm of
         Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     let val pth =
           (* If quick_and_dirty then run without proof generation as oracle*)
              if Config.get ctxt quick_and_dirty
-             then mirfr_oracle (false, Thm.global_cterm_of thy (Envir.eta_long [] t1))
-             else mirfr_oracle (true, Thm.global_cterm_of thy (Envir.eta_long [] t1))
+             then mirfr_oracle (false, Thm.cterm_of ctxt (Envir.eta_long [] t1))
+             else mirfr_oracle (true, Thm.cterm_of ctxt (Envir.eta_long [] t1))
     in 
        ((pth RS iffD2) RS pre_thm,
         assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
     end
       | _ => (pre_thm, assm_tac i)