diff -r 7319d384d0d3 -r 0c90e581379f src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Tue Dec 18 21:28:01 2001 +0100
+++ b/src/HOL/IMP/Compiler.thy	Wed Dec 19 00:26:04 2001 +0100
@@ -19,15 +19,15 @@
 consts  stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
 
 syntax
-  "@stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
                ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)
-  "@stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
                ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)
 
 syntax (xsymbols)
-  "@stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
                ("_ \<turnstile> \<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
-  "@stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
                ("_ \<turnstile>/ \<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
 
 translations