# HG changeset patch
# User oheimb
# Date 946904830 -3600
# Node ID f0d4165bc534a152f2906aeafe3eceb3ef87d64c
# Parent  381716a86fcb9f81fe24a521631c123cfcfc2c49
removed inj_eq from the default simpset again

diff -r 381716a86fcb -r f0d4165bc534 src/HOL/MicroJava/J/JBasis.ML
--- a/src/HOL/MicroJava/J/JBasis.ML	Mon Jan 03 14:07:08 2000 +0100
+++ b/src/HOL/MicroJava/J/JBasis.ML	Mon Jan 03 14:07:10 2000 +0100
@@ -67,10 +67,6 @@
 		rotate_tac ~1,asm_full_simp_tac 
 	(simpset() delsimps [split_paired_All,split_paired_Ex])];
 
-Goal "{y. x = Some y} \\<subseteq> {the x}";
-by Auto_tac;
-qed "some_subset_the";
-
 fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1,
   asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];