diff -r f7157bdc1e70 -r 8f32860eac3a src/HOL/NanoJava/Term.thy
--- a/src/HOL/NanoJava/Term.thy	Wed Aug 08 15:16:38 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy	Wed Aug 08 16:57:43 2001 +0200
@@ -38,11 +38,5 @@
   | Call cname expr mname expr                   (* method call      *)
                      ("{_}_.._'(_')" [99,95,99,95] 95)
 
-
-lemma pair_imageI [intro]: "(a, b) \<in> A ==> f a b : (%(a, b). f a b) ` A"
-apply (rule_tac x = "(a,b)" in image_eqI)
-apply  auto
-done
-
 end