# HG changeset patch
# User schirmer
# Date 1096513697 -7200
# Node ID 15fa818ef6240439a7aac7929202e139145633c6
# Parent  2fac1f11b7f6b667ada4f55b6f674d6b7d94d235
bug-fix with new records

diff -r 2fac1f11b7f6 -r 15fa818ef624 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Wed Sep 29 22:40:40 2004 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Thu Sep 30 05:08:17 2004 +0200
@@ -263,7 +263,7 @@
   (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)"
 apply (unfold init_obj_def)
 apply (auto elim!: conforms_gupd dest!: oconf_init_obj 
-            simp add: obj.update_defs)
+            )
 done
 
 lemma conforms_init_class_obj: