--- 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