--- a/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 06 15:58:56 2015 +0100
@@ -101,7 +101,7 @@
@{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.cterm_of thy (HOLogic.mk_Trueprop t)
+ val ct = Thm.global_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,
@@ -116,8 +116,8 @@
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 thy (Envir.eta_long [] t1))
- else mirfr_oracle (true, Thm.cterm_of thy (Envir.eta_long [] t1))
+ 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))
in
((pth RS iffD2) RS pre_thm,
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))