diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon May 26 18:36:15 2003 +0200
@@ -186,6 +186,7 @@
 text {*
   The program is structurally wellformed:
 *}
+
 lemma wf_struct:
   "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
 proof -
@@ -223,7 +224,8 @@
     apply (auto simp add: name_defs distinct_classes distinct_fields)
     done       
   ultimately
-  show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def)
+  show ?thesis 
+    by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def)
 qed
 
 section "Welltypings"