--- a/src/HOL/Tools/SMT/smt_config.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Thu Mar 15 20:07:00 2012 +0100
@@ -86,7 +86,7 @@
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))
@@ -142,7 +142,7 @@
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"
@@ -207,7 +207,7 @@
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"