src/HOL/Tools/SMT/smt_solver.ML
changeset 38808 89ae86205739
parent 36960 01594f816e3a
child 39483 9f0e5684f04b
     1.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Aug 27 17:23:57 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Aug 27 17:59:40 2010 +0200
     1.3 @@ -310,18 +310,18 @@
     1.4  (* setup *)
     1.5  
     1.6  val setup =
     1.7 -  Attrib.setup (Binding.name "smt_solver")
     1.8 +  Attrib.setup @{binding smt_solver}
     1.9      (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
    1.10        (Thm.declaration_attribute o K o select_solver))
    1.11      "SMT solver configuration" #>
    1.12    setup_timeout #>
    1.13    setup_trace #>
    1.14    setup_fixed_certificates #>
    1.15 -  Attrib.setup (Binding.name "smt_certificates")
    1.16 +  Attrib.setup @{binding smt_certificates}
    1.17      (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
    1.18        (Thm.declaration_attribute o K o select_certificates))
    1.19      "SMT certificates" #>
    1.20 -  Method.setup (Binding.name "smt") smt_method
    1.21 +  Method.setup @{binding smt} smt_method
    1.22      "Applies an SMT solver to the current goal."
    1.23  
    1.24