src/HOL/BNF_Def.thy

--- a/src/HOL/BNF_Def.thy	Fri Feb 28 12:04:40 2014 +0100
+++ b/src/HOL/BNF_Def.thy	Tue Feb 25 18:14:26 2014 +0100
@@ -137,9 +137,6 @@
   ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i"
 unfolding Func_def by (auto elim: the_inv_into_f_f)
 
-definition vimage2p where
-  "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
-
 lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
   unfolding vimage2p_def by -