src/HOL/Tools/SMT/z3_isar.ML

           in
             (name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines
           end
       end
 
-fun dest_alls (Const (@{const_name Pure.all}, _) $ Abs (abs as (_, T, _))) =
+fun dest_alls (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (abs as (_, T, _))) =
     let val (s', t') = Term.dest_abs abs in
       dest_alls t' |>> cons (s', T)
     end
   | dest_alls t = ([], t)