src/HOL/Tools/SMT/smt_real.ML

--- a/src/HOL/Tools/SMT/smt_real.ML	Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Mar 04 22:05:01 2015 +0100
@@ -89,7 +89,7 @@
   mk_builtin_typ = z3_mk_builtin_typ,
   mk_builtin_num = z3_mk_builtin_num,
   mk_builtin_fun = (fn _ => fn sym => fn cts =>
-    (case try (#T o Thm.rep_cterm o hd) cts of
+    (case try (Thm.typ_of_cterm o hd) cts of
       SOME @{typ real} => z3_mk_builtin_fun sym cts
     | _ => NONE)) }