# HG changeset patch
# User nipkow
# Date 944122170 -3600
# Node ID 3a0c996cf2b2a3dc46f0ca57058c7f0d7076d167
# Parent  91587887bcbfcb190086f16a8fd3b9f4851ea804
cosmetic mod.

diff -r 91587887bcbf -r 3a0c996cf2b2 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Wed Dec 01 22:38:35 1999 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Dec 02 09:09:30 1999 +0100
@@ -41,7 +41,7 @@
          fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and>
          length apTs = length pTs \\<and>
          (\\<exists>D' rT' maxl' ins'.
-           method (G,D) (mn,pTs) = Some(D',rT',(maxl',ins')) \\<and>
+           method (G,D) sig0 = Some(D',rT',(maxl',ins')) \\<and>
            G \\<turnstile> rT0 \\<preceq> rT') \\<and>
 	 correct_frame G hp (tl ST, LT) maxl ins f \\<and> 
 	 correct_frames G hp phi rT sig frs))))"