src/HOL/Tools/SMT/smt_normalize.ML
changeset 46497 89ccf66aa73d
parent 44890 22f665a2e91c
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Feb 15 22:44:31 2012 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Feb 15 23:19:30 2012 +0100
     1.3 @@ -196,7 +196,7 @@
     1.4  
     1.5    val pat =
     1.6      SMT_Utils.mk_const_pat @{theory} @{const_name SMT.pat} SMT_Utils.destT1
     1.7 -  fun mk_pat ct = Thm.capply (SMT_Utils.instT' ct pat) ct
     1.8 +  fun mk_pat ct = Thm.apply (SMT_Utils.instT' ct pat) ct
     1.9  
    1.10    fun mk_clist T = pairself (Thm.cterm_of @{theory})
    1.11      (HOLogic.cons_const T, HOLogic.nil_const T)