diff -r 92d7d8e4f1bf -r 291934bac95e src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Fri Mar 06 15:58:56 2015 +0100
@@ -5655,7 +5655,7 @@
     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.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
+  in (Thm.global_cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
 end;
 *}