src/HOL/Tools/SMT/smt_translate.ML
changeset 43507 d566714a9ce1
parent 43385 9cd4b4ecb4dd
child 43554 9bece8cbb5be
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Jun 21 23:08:16 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Jun 22 15:07:03 2011 +0200
     1.3 @@ -38,6 +38,8 @@
     1.4    (*translation*)
     1.5    val add_config: SMT_Utils.class * (Proof.context -> config) ->
     1.6      Context.generic -> Context.generic 
     1.7 +  val lift_lambdas: Proof.context -> term list ->
     1.8 +    Proof.context * (term list * term list)
     1.9    val translate: Proof.context -> string list -> (int * thm) list ->
    1.10      string * recon
    1.11  end
    1.12 @@ -308,7 +310,7 @@
    1.13    (Termtab.empty, ctxt)
    1.14    |> fold_map (traverse []) ts
    1.15    |> (fn (us, (defs, ctxt')) =>
    1.16 -       (ctxt', Termtab.fold (cons o snd o snd) defs us))
    1.17 +       (ctxt', (Termtab.fold (cons o snd o snd) defs [], us)))
    1.18  
    1.19  end
    1.20  
    1.21 @@ -588,6 +590,7 @@
    1.22        ts2
    1.23        |> eta_expand ctxt1 is_fol funcs
    1.24        |> lift_lambdas ctxt1
    1.25 +      ||> (op @)
    1.26        |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs)
    1.27  
    1.28      val ((rewrite_rules, extra_thms, builtin), ts4) =