--- a/src/HOL/Tools/BNF/bnf_tactics.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML Fri Jan 04 23:22:53 2019 +0100
@@ -44,7 +44,7 @@
end
handle Pattern.MATCH => no_tac) ctxt;
-fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
+fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of \<^theory_context>\<open>HOL\<close>) ctxt);
(*unlike "unfold_thms_tac", it succeed when the RHS contains schematic variables not in the LHS*)
fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];