# HG changeset patch
# User bulwahn
# Date 1242497906 -7200
# Node ID 9b1e7159f4e51b857ff86983570c9be604715226
# Parent  f1f1e9b53c816f3ce821db299e666e280d5bd4a3# Parent  138eae50855610ed750fbcae1b65daa77656e4e5
merged

diff -r f1f1e9b53c81 -r 9b1e7159f4e5 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Sat May 16 20:17:59 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sat May 16 20:18:26 2009 +0200
@@ -69,10 +69,9 @@
 lemma subcls1:
   "subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
                 (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})"
-apply (simp add: subcls1_def2)
+apply (simp add: subcls1_def2 del:singleton_conj_conv2)
 apply (simp add: name_defs class_defs system_defs E_def class_def)
-apply (auto simp: expand_fun_eq name_defs[symmetric] class_defs split:split_if_asm)
-apply(simp add:name_defs)+
+apply (auto simp: expand_fun_eq split: split_if_asm)
 done
 
 text {* The subclass relation is acyclic; hence its converse is well founded: *}