diff -r d09c66a0ea10 -r 6c28d8ed2488 src/HOL/ex/MT.thy
--- a/src/HOL/ex/MT.thy	Thu Jul 23 22:13:42 2015 +0200
+++ b/src/HOL/ex/MT.thy	Fri Jul 24 22:16:39 2015 +0200
@@ -276,7 +276,7 @@
 (* ############################################################ *)
 
 ML {*
-val infsys_mono_tac = REPEAT (ares_tac (@{thms basic_monos} @ [allI, impI]) 1)
+fun infsys_mono_tac ctxt = REPEAT (ares_tac ctxt (@{thms basic_monos} @ [allI, impI]) 1)
 *}
 
 lemma infsys_p1: "P a b ==> P (fst (a,b)) (snd (a,b))"
@@ -395,7 +395,7 @@
 
 lemma eval_fun_mono: "mono(eval_fun)"
 unfolding mono_def eval_fun_def
-apply (tactic infsys_mono_tac)
+apply (tactic "infsys_mono_tac @{context}")
 done
 
 (* Introduction rules *)
@@ -519,7 +519,7 @@
 
 lemma elab_fun_mono: "mono(elab_fun)"
 unfolding mono_def elab_fun_def
-apply (tactic infsys_mono_tac)
+apply (tactic "infsys_mono_tac @{context}")
 done
 
 (* Introduction rules *)
@@ -747,7 +747,7 @@
 
 lemma mono_hasty_fun: "mono(hasty_fun)"
 unfolding mono_def hasty_fun_def
-apply (tactic infsys_mono_tac)
+apply (tactic "infsys_mono_tac @{context}")
 apply blast
 done