src/HOL/Complex/ex/mirtac.ML

 val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
 val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
 val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
 val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;
 
-fun prepare_for_mir sg q fm = 
+fun prepare_for_mir thy q fm = 
   let
     val ps = Logic.strip_params fm
     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
     fun mk_all ((s, T), (P,n)) =

 	THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
 	THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
 	THEN (fn st =>
   let
     val g = List.nth (prems_of st, i - 1)
-    val sg = ProofContext.theory_of ctxt
+    val thy = ProofContext.theory_of ctxt
     (* Transform the term*)
-    val (t,np,nh) = prepare_for_mir sg q g
+    val (t,np,nh) = prepare_for_mir thy q g
     (* Some simpsets for dealing with mod div abs and nat*)
     val mod_div_simpset = HOL_basic_ss 
 			addsimps [refl,nat_mod_add_eq, 
 				  @{thm "mod_self"}, @{thm "zmod_self"},
 				  @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},

     val simpset2 = HOL_basic_ss
       addsimps [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
                 @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}]
       addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
     (* simp rules for elimination of abs *)
-    val ct = cterm_of sg (HOLogic.mk_Trueprop t)
+    val ct = cterm_of thy (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 mir_ss 1)]
       (trivial ct))

     val (th, tac) = case (prop_of pre_thm) of
         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
     let val pth = 
           (* If quick_and_dirty then run without proof generation as oracle*)
              if !quick_and_dirty 
-             then mircfr_oracle sg (Pattern.eta_long [] t1)
-	     else mirlfr_oracle sg (Pattern.eta_long [] t1)
+             then mirfr_oracle thy (false, Pattern.eta_long [] t1)
+	     else mirfr_oracle thy (true, Pattern.eta_long [] t1)
     in 
           (trace_msg ("calling procedure with term:\n" ^
              Syntax.string_of_term ctxt t1);
            ((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)
   in (rtac (((mp_step nh) o (spec_step np)) th) i 
       THEN tac) st
-  end handle Subscript => no_tac st | ReflectedMir.MIR => no_tac st);
+  end handle Subscript => no_tac st);
 
 fun mir_args meth =
  let val parse_flag = 
          Args.$$$ "no_quantify" >> (K (K false));
  in