--- a/src/FOL/ex/Miniscope.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/FOL/ex/Miniscope.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -68,7 +68,7 @@
 lemmas mini_simps = demorgans nnf_simps ex_simps all_simps
 
 ML \<open>
-val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps});
+val mini_ss = simpset_of (\<^context> addsimps @{thms mini_simps});
 fun mini_tac ctxt =
   resolve_tac ctxt @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
 \<close>