src/HOL/Set.thy

--- a/src/HOL/Set.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Set.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -1586,8 +1586,7 @@
 
 subsubsection {* Inverse image of a function *}
 
-constdefs
-  vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
+definition vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90) where
   [code del]: "f -` B == {x. f x : B}"
 
 lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"