--- a/src/HOL/HoareParallel/RG_Com.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HoareParallel/RG_Com.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
 \section {Abstract Syntax}
 *}
 
-theory RG_Com = Main:
+theory RG_Com imports Main begin
 
 text {* Semantics of assertions and boolean expressions (bexp) as sets
 of states.  Syntax of commands @{text com} and parallel commands