src/HOL/Tools/SMT/smt_real.ML
changeset 66551 4df6b0ae900d
parent 62913 13252110a6fe
child 69205 8050734eee3e
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Tue Aug 29 16:24:14 2017 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Tue Aug 29 18:30:23 2017 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  
     1.5  val setup_builtins =
     1.6    SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
     1.7 -    (@{typ real}, K (SOME "Real"), real_num) #>
     1.8 +    (@{typ real}, K (SOME ("Real", [])), real_num) #>
     1.9    fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
    1.10      (@{const less (real)}, "<"),
    1.11      (@{const less_eq (real)}, "<="),