| changeset 46497 | 89ccf66aa73d |
| parent 42361 | 23f352990944 |
| child 54489 | 03ff4d1e6784 |
--- a/src/HOL/Tools/SMT/smt_utils.ML Wed Feb 15 22:44:31 2012 +0100 +++ b/src/HOL/Tools/SMT/smt_utils.ML Wed Feb 15 23:19:30 2012 +0100 @@ -182,7 +182,7 @@ val dest_all_cbinders = repeat_yield (try o dest_cbinder) -val mk_cprop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop}) +val mk_cprop = Thm.apply (Thm.cterm_of @{theory} @{const Trueprop}) fun dest_cprop ct = (case Thm.term_of ct of