src/HOL/Tools/SMT/smt_real.ML
changeset 41302 0485186839a7
parent 41281 679118e35378
child 41439 a31c451183e6
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Mon Dec 20 08:45:27 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Mon Dec 20 09:06:37 2010 +0100
     1.3 @@ -39,12 +39,6 @@
     1.4  
     1.5    fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
     1.6      | times _ _ _  = NONE
     1.7 -
     1.8 -  fun mk_divide ts = Term.list_comb (@{const divide (real)}, ts)
     1.9 -
    1.10 -  fun divide _ T (ts as [_, t]) =
    1.11 -        if U.is_number t then SOME ("/", 2, ts, mk_divide) else NONE
    1.12 -    | divide _ _ _ = NONE
    1.13  in
    1.14  
    1.15  val setup_builtins =
    1.16 @@ -57,8 +51,8 @@
    1.17      (@{const minus (real)}, "-") ] #>
    1.18    B.add_builtin_fun SMTLIB_Interface.smtlibC
    1.19      (Term.dest_Const @{const times (real)}, times) #>
    1.20 -  B.add_builtin_fun Z3_Interface.smtlib_z3C
    1.21 -    (Term.dest_Const @{const divide (real)}, divide)
    1.22 +  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const times (real)}, "*") #>
    1.23 +  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/")
    1.24  
    1.25  end
    1.26