diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/JVM/JVMExec.thy
--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -34,6 +34,6 @@
 
 syntax (xsymbols)
   exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
-              ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
+              ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
 
 end