src/HOL/SMT.thy

--- a/src/HOL/SMT.thy	Wed Dec 15 08:39:24 2010 +0100
+++ b/src/HOL/SMT.thy	Wed Dec 15 10:12:44 2010 +0100
@@ -91,7 +91,7 @@
 following constant.
 *}
 
-definition fun_app where "fun_app f x = f x"
+definition fun_app where "fun_app f = f"
 
 text {*
 Some solvers support a theory of arrays which can be used to encode