# 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)\\(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: