src/HOL/Tools/SMT/z3_replay.ML

   let
     val (ns, ctxt') = Variable.variant_fixes (replicate (length nTs) "") ctxt
     fun mk (n, T) n' = (n, Thm.cterm_of ctxt' (Free (n', T)))
   in (ctxt', Symtab.make (map2 mk nTs ns)) end
 
-fun forall_elim_term ct (Const (@{const_name Pure.all}, _) $ (a as Abs _)) =
+fun forall_elim_term ct (Const (\<^const_name>\<open>Pure.all\<close>, _) $ (a as Abs _)) =
       Term.betapply (a, Thm.term_of ct)
   | forall_elim_term _ qt = raise TERM ("forall_elim'", [qt])
 
 fun apply_fixes elim env = fold (elim o the o Symtab.lookup env)