Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/SMT/smt_translate.ML
changeset 40697 c3979dd80a50
parent 40681 872b08416fb4
child 41057 8dbc951a291c 
--- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Nov 25 14:13:48 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Nov 25 14:58:20 2010 +0100
@@ -402,6 +402,9 @@
               | NONE => transs h T ts))
       | (h as Free (_, T), ts) => transs h T ts
       | (Bound i, []) => pair (SVar i)
+      | (Abs (_, _, t1 $ Bound 0), []) =>
+        if not (loose_bvar1 (t1, 0)) then trans t1 (* eta-reduce on the fly *)
+        else raise TERM ("smt_translate", [t])
       | _ => raise TERM ("smt_translate", [t]))
 
     and transs t T ts =
isabelle