--- a/src/HOL/IMP/Procs.thy Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Procs.thy Thu Oct 20 09:48:00 2011 +0200
@@ -4,15 +4,17 @@
subsection "Procedures and Local Variables"
+type_synonym pname = string
+
datatype
com = SKIP
- | Assign name aexp ("_ ::= _" [1000, 61] 61)
+ | Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Semi 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 name com ("(1{VAR _;;/ _})")
- | Proc name com com ("(1{PROC _ = _;;/ _})")
- | CALL name
+ | Var vname com ("(1{VAR _;;/ _})")
+ | Proc pname com com ("(1{PROC _ = _;;/ _})")
+ | CALL pname
definition "test_com =
{VAR ''x'';;