src/HOL/SMT.thy
changeset 41127 2ea84c8535c6
parent 41126 e0bd443c0fdd
child 41174 10eb369f8c01
     1.1 --- a/src/HOL/SMT.thy	Wed Dec 15 08:39:24 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Wed Dec 15 10:12:44 2010 +0100
     1.3 @@ -91,7 +91,7 @@
     1.4  following constant.
     1.5  *}
     1.6  
     1.7 -definition fun_app where "fun_app f x = f x"
     1.8 +definition fun_app where "fun_app f = f"
     1.9  
    1.10  text {*
    1.11  Some solvers support a theory of arrays which can be used to encode