src/HOL/Tools/SMT/smt_config.ML

     error ("Solver already registered: " ^ quote name)
   else
     context
     |> Solvers.map (apfst (Symtab.update (name, (info, []))))
     |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
-        (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+        (Scan.lift (@{keyword "="} |-- Args.name) >>
           (Thm.declaration_attribute o K o set_solver_options o pair name))
         ("Additional command line options for SMT solver " ^ quote name))
 
 fun all_solvers_of ctxt = Symtab.keys (fst (Solvers.get (Context.Proof ctxt)))
 

           opts @ options ctxt
   in solver_info_of (K []) all_options ctxt end
 
 val setup_solver =
   Attrib.setup @{binding smt_solver}
-    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+    (Scan.lift (@{keyword "="} |-- Args.name) >>
       (Thm.declaration_attribute o K o select_solver))
     "SMT solver configuration"
 
 
 (* options *)

 
 val certificates_of = Certificates.get o Context.Proof
 
 val setup_certificates =
   Attrib.setup @{binding smt_certificates}
-    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+    (Scan.lift (@{keyword "="} |-- Args.name) >>
       (Thm.declaration_attribute o K o select_certificates))
     "SMT certificates configuration"
 
 
 (* setup *)