src/HOL/Tools/SMT/smt_translate.ML
changeset 40697 c3979dd80a50
parent 40681 872b08416fb4
child 41057 8dbc951a291c
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Nov 25 14:13:48 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Nov 25 14:58:20 2010 +0100
     1.3 @@ -402,6 +402,9 @@
     1.4                | NONE => transs h T ts))
     1.5        | (h as Free (_, T), ts) => transs h T ts
     1.6        | (Bound i, []) => pair (SVar i)
     1.7 +      | (Abs (_, _, t1 $ Bound 0), []) =>
     1.8 +        if not (loose_bvar1 (t1, 0)) then trans t1 (* eta-reduce on the fly *)
     1.9 +        else raise TERM ("smt_translate", [t])
    1.10        | _ => raise TERM ("smt_translate", [t]))
    1.11  
    1.12      and transs t T ts =