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