Branch: top elements of stack only need to be convertible (not equal)

--- a/src/HOL/MicroJava/BV/BVSpec.thy	Sat Feb 05 17:06:27 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Sat Feb 05 17:31:53 2000 +0100
@@ -136,9 +136,10 @@
 	(let (ST,LT) = phi ! pc
 	 in
 	 pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and> 
-	 (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and>  ts = ts' \\<and>
+	 (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and>  (G \\<turnstile> ts \\<preceq> ts' \\<or> G \\<turnstile> ts' \\<preceq> ts) \\<and>
 		       G \\<turnstile> (ST' , LT) <=s phi ! (pc+1) \\<and>
 		       G \\<turnstile> (ST' , LT) <=s phi ! (nat(int pc+branch))))"
+
 "wt_BR (Goto branch) G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
 	 in