diff -r 72b5d28aae58 -r f58863b1406a src/HOL/TLA/Memory/ProcedureInterface.thy
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Thu Aug 03 19:28:37 2000 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Thu Aug 03 19:29:03 2000 +0200
@@ -69,11 +69,11 @@
 
   Calling_def	"Calling ch p  == PRED cbit< ch!p > ~= rbit< ch!p >"
   Call_def      "(ACT Call ch p v)   == ACT  ~ $Calling ch p
-                                     & (cbit<ch!p>` ~= $rbit<ch!p>)
-                                     & (arg<ch!p>` = $v)"
+                                     & (cbit<ch!p>$ ~= $rbit<ch!p>)
+                                     & (arg<ch!p>$ = $v)"
   Return_def    "(ACT Return ch p v) == ACT  $Calling ch p
-                                     & (rbit<ch!p>` = $cbit<ch!p>)
-                                     & (res<ch!p>` = $v)"
+                                     & (rbit<ch!p>$ = $cbit<ch!p>)
+                                     & (res<ch!p>$ = $v)"
   PLegalCaller_def      "PLegalCaller ch p == TEMP
                              Init(~ Calling ch p)
                              & [][ ? a. Call ch p a ]_((caller ch)!p)"