1.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Feb 15 22:44:31 2012 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Feb 15 23:19:30 2012 +0100
     1.3 @@ -116,7 +116,7 @@
     1.4    let
     1.5      val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
     1.6      val (cf, cvs) = Drule.strip_comb lhs
     1.7 -    val eq = SMT_Utils.mk_cequals cf (fold_rev Thm.cabs cvs rhs)
     1.8 +    val eq = SMT_Utils.mk_cequals cf (fold_rev Thm.lambda cvs rhs)
     1.9      fun apply cv th =
    1.10        Thm.combination th (Thm.reflexive cv)
    1.11        |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
    1.12 @@ -159,14 +159,14 @@
    1.13            val cv = SMT_Utils.certify ctxt'
    1.14              (Free (n, map SMT_Utils.typ_of cvs' ---> SMT_Utils.typ_of ct))
    1.15            val cu = Drule.list_comb (cv, cvs')
    1.16 -          val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
    1.17 +          val e = (t, (cv, fold_rev Thm.lambda cvs' ct))
    1.18            val beta_norm' = beta_norm orelse not (null cvs')
    1.19          in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
    1.20    end
    1.21  
    1.22  fun abs_comb f g dcvs ct =
    1.23    let val (cf, cu) = Thm.dest_comb ct
    1.24 -  in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.capply end
    1.25 +  in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.apply end
    1.26  
    1.27  fun abs_arg f = abs_comb (K pair) f
    1.28  
    1.29 @@ -184,7 +184,7 @@
    1.30  
    1.31  fun abs_abs f (depth, cvs) ct =
    1.32    let val (cv, cu) = Thm.dest_abs NONE ct
    1.33 -  in f (depth, cv :: cvs) cu #>> Thm.cabs cv end
    1.34 +  in f (depth, cv :: cvs) cu #>> Thm.lambda cv end
    1.35  
    1.36  val is_atomic =
    1.37    (fn Free _ => true | Var _ => true | Bound _ => true | _ => false)