src/HOL/Tools/SMT/smt_real.ML
changeset 59586 ddf6deaadfe8
parent 58061 3d060f43accb
child 59621 291934bac95e
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Wed Mar 04 20:50:20 2015 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Mar 04 22:05:01 2015 +0100
     1.3 @@ -89,7 +89,7 @@
     1.4    mk_builtin_typ = z3_mk_builtin_typ,
     1.5    mk_builtin_num = z3_mk_builtin_num,
     1.6    mk_builtin_fun = (fn _ => fn sym => fn cts =>
     1.7 -    (case try (#T o Thm.rep_cterm o hd) cts of
     1.8 +    (case try (Thm.typ_of_cterm o hd) cts of
     1.9        SOME @{typ real} => z3_mk_builtin_fun sym cts
    1.10      | _ => NONE)) }
    1.11