
diff -r e1fce873b814 -r d797baa3d57c src/HOL/Hoare_Parallel/OG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Dec 17 17:43:54 2010 +0100
@@ -56,8 +56,7 @@
   "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT CONST True THEN c END"
   "r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END"
  
-nonterminals
-  prgs
+nonterminal prgs
 
 syntax
   "_PAR" :: "prgs \<Rightarrow> 'a"              ("COBEGIN//_//COEND" [57] 56)




