equal
deleted
inserted
replaced
95 |
95 |
96 val z3_mk_builtins = { |
96 val z3_mk_builtins = { |
97 mk_builtin_typ = z3_mk_builtin_typ, |
97 mk_builtin_typ = z3_mk_builtin_typ, |
98 mk_builtin_num = z3_mk_builtin_num, |
98 mk_builtin_num = z3_mk_builtin_num, |
99 mk_builtin_fun = (fn _ => fn sym => fn cts => |
99 mk_builtin_fun = (fn _ => fn sym => fn cts => |
100 (case try (#T o Thm.rep_cterm o hd) cts of |
100 (case try (Thm.typ_of_cterm o hd) cts of |
101 SOME @{typ real} => z3_mk_builtin_fun sym cts |
101 SOME @{typ real} => z3_mk_builtin_fun sym cts |
102 | _ => NONE)) } |
102 | _ => NONE)) } |
103 |
103 |
104 end |
104 end |
105 |
105 |