1.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Feb 15 22:44:31 2012 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Feb 15 23:19:30 2012 +0100
     1.3 @@ -134,7 +134,7 @@
     1.4          | _ => SMT_Utils.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T)))
     1.5        fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
     1.6        val vars' = map_filter dec vars
     1.7 -    in (Thm.capply (SMT_Utils.instT' cv q) (Thm.cabs cv ct), vars') end
     1.8 +    in (Thm.apply (SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end
     1.9  
    1.10    fun quant name =
    1.11      SMT_Utils.mk_const_pat @{theory} name (SMT_Utils.destT1 o SMT_Utils.destT1)