diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Procs.thy
--- a/src/HOL/IMP/Procs.thy	Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Procs.thy	Fri May 17 08:19:52 2013 +0200
@@ -9,20 +9,20 @@
 datatype
   com = SKIP 
       | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
-      | Seq    com  com          ("_;/ _"  [60, 61] 60)
+      | Seq    com  com          ("_;;/ _"  [60, 61] 60)
       | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
       | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
-      | Var    vname com        ("(1{VAR _;;/ _})")
-      | Proc   pname com com    ("(1{PROC _ = _;;/ _})")
+      | Var    vname com        ("(1{VAR _;/ _})")
+      | Proc   pname com com    ("(1{PROC _ = _;/ _})")
       | CALL   pname
 
 definition "test_com =
-{VAR ''x'';;
- {PROC ''p'' = ''x'' ::= N 1;;
-  {PROC ''q'' = CALL ''p'';;
-   {VAR ''x'';;
-    ''x'' ::= N 2;
-    {PROC ''p'' = ''x'' ::= N 3;;
-     CALL ''q''; ''y'' ::= V ''x''}}}}}"
+{VAR ''x'';
+ {PROC ''p'' = ''x'' ::= N 1;
+  {PROC ''q'' = CALL ''p'';
+   {VAR ''x'';
+    ''x'' ::= N 2;;
+    {PROC ''p'' = ''x'' ::= N 3;
+     CALL ''q'';; ''y'' ::= V ''x''}}}}}"
 
 end