clarified context;

--- a/src/HOL/Decision_Procs/Cooper.thy	Mon Jun 01 10:47:08 2015 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Jun 01 11:46:03 2015 +0200
@@ -2640,16 +2640,14 @@
   end;
 
 in
-  fn ct =>
+  fn (ctxt, t) =>
     let
-      val thy = Thm.theory_of_cterm ct;
-      val t = Thm.term_of ct;
       val fs = Misc_Legacy.term_frees t;
       val bs = term_bools [] t;
       val vs = map_index swap fs;
       val ps = map_index swap bs;
-      val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
-    in Thm.global_cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
+      val t' = term_of_fm ps vs (@{code pa} (fm_of_term ps vs t));
+    in Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
 end;
 *}
 

--- a/src/HOL/Decision_Procs/MIR.thy	Mon Jun 01 10:47:08 2015 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Mon Jun 01 11:46:03 2015 +0200
@@ -5532,7 +5532,7 @@
   functions mircfrqe mirlfrqe
   file "mir.ML"*)
 
-oracle mirfr_oracle = {* fn (proofs, ct) =>
+oracle mirfr_oracle = {*
 let
 
 val mk_C = @{code C} o @{code int_of_integer};
@@ -5648,14 +5648,14 @@
       @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ term_of_fm vs t1 $ term_of_fm vs t2;
 
 in
+  fn (ctxt, t) =>
   let 
-    val thy = Thm.theory_of_cterm ct;
-    val t = Thm.term_of ct;
     val fs = Misc_Legacy.term_frees t;
     val vs = map_index swap fs;
-    val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
-    val t' = (term_of_fm vs o qe o fm_of_term vs) t;
-  in (Thm.global_cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
+    (*If quick_and_dirty then run without proof generation as oracle*)
+    val qe = if Config.get ctxt quick_and_dirty then @{code mircfrqe} else @{code mirlfrqe};
+    val t' = term_of_fm vs (qe (fm_of_term vs t));
+  in Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
 end;
 *}
 

--- a/src/HOL/Decision_Procs/cooper_tac.ML	Mon Jun 01 10:47:08 2015 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Mon Jun 01 11:46:03 2015 +0200
@@ -85,7 +85,7 @@
       (case Thm.prop_of pre_thm of
         Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
           let
-            val pth = linzqe_oracle (Thm.cterm_of ctxt (Envir.eta_long [] t1))
+            val pth = linzqe_oracle (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))

--- a/src/HOL/Decision_Procs/mir_tac.ML	Mon Jun 01 10:47:08 2015 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Mon Jun 01 11:46:03 2015 +0200
@@ -112,11 +112,8 @@
     val (th, tac) =
       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.cterm_of ctxt (Envir.eta_long [] t1))
-             else mirfr_oracle (true, Thm.cterm_of ctxt (Envir.eta_long [] t1))
+    let
+      val pth = mirfr_oracle (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))