diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Mar 05 12:31:31 2001 +0100
+++ b/src/HOL/IsaMakefile	Mon Mar 05 15:25:11 2001 +0100
@@ -320,28 +320,39 @@
 HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
 
 $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
-  UNITY/Alloc.ML UNITY/Alloc.thy UNITY/AllocBase.ML UNITY/AllocBase.thy \
-  UNITY/Channel.ML UNITY/Channel.thy UNITY/Client.ML UNITY/Client.thy \
-  UNITY/Common.ML UNITY/Common.thy UNITY/Comp.ML UNITY/Comp.thy \
-  UNITY/Counter.ML UNITY/Counter.thy UNITY/Counterc.ML UNITY/Counterc.thy \
-  UNITY/Deadlock.ML UNITY/Deadlock.thy UNITY/Detects.ML \
-  UNITY/Detects.thy UNITY/ELT.ML UNITY/ELT.thy UNITY/Extend.ML \
+  UNITY/Comp.ML UNITY/Comp.thy \
+  UNITY/Detects.ML UNITY/Detects.thy \
+  UNITY/ELT.ML UNITY/ELT.thy UNITY/Extend.ML \
   UNITY/Extend.thy UNITY/FP.ML UNITY/FP.thy UNITY/Follows.ML \
   UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \
-  UNITY/Guar.ML UNITY/Guar.thy UNITY/Handshake.ML UNITY/Handshake.thy \
-  UNITY/Lift.ML UNITY/Lift.thy UNITY/Lift_prog.ML UNITY/Lift_prog.thy \
-  UNITY/ListOrder.thy UNITY/Mutex.ML UNITY/Mutex.thy UNITY/NSP_Bad.ML \
-  UNITY/NSP_Bad.thy UNITY/Network.ML UNITY/Network.thy  \
+  UNITY/Guar.ML UNITY/Guar.thy  \
+  UNITY/Lift_prog.ML UNITY/Lift_prog.thy \
+  UNITY/ListOrder.thy  \
   UNITY/PPROD.ML UNITY/PPROD.thy \
-  UNITY/PriorityAux.ML UNITY/PriorityAux.thy \
-  UNITY/Priority.ML UNITY/Priority.thy \
   UNITY/Project.ML UNITY/Project.thy \
-  UNITY/Reach.ML UNITY/Reach.thy UNITY/Reachability.ML \
-  UNITY/Reachability.thy UNITY/Rename.ML UNITY/Rename.thy \
-  UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/TimerArray.ML \
-  UNITY/TimerArray.thy UNITY/Token.ML UNITY/Token.thy UNITY/UNITY.ML \
+  UNITY/Rename.ML UNITY/Rename.thy \
+  UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML \
   UNITY/UNITY.thy UNITY/Union.ML UNITY/Union.thy UNITY/WFair.ML \
-  UNITY/WFair.thy
+  UNITY/WFair.thy \
+  UNITY/Simple/Channel.ML UNITY/Simple/Channel.thy  \
+  UNITY/Simple/Common.ML UNITY/Simple/Common.thy  \
+  UNITY/Simple/Deadlock.ML UNITY/Simple/Deadlock.thy  \
+  UNITY/Simple/Lift.ML UNITY/Simple/Lift.thy  \
+  UNITY/Simple/Mutex.ML UNITY/Simple/Mutex.thy  \
+  UNITY/Simple/NSP_Bad.ML UNITY/Simple/NSP_Bad.thy  \
+  UNITY/Simple/Network.ML UNITY/Simple/Network.thy  \
+  UNITY/Simple/Reach.ML UNITY/Simple/Reach.thy   \
+  UNITY/Simple/Reachability.ML UNITY/Simple/Reachability.thy   \
+  UNITY/Simple/Token.ML UNITY/Simple/Token.thy \
+  UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \
+  UNITY/Comp/AllocBase.ML UNITY/Comp/AllocBase.thy \
+  UNITY/Comp/Client.ML UNITY/Comp/Client.thy \
+  UNITY/Comp/Counter.ML UNITY/Comp/Counter.thy \
+  UNITY/Comp/Counterc.ML UNITY/Comp/Counterc.thy \
+  UNITY/Comp/Handshake.ML UNITY/Comp/Handshake.thy \
+  UNITY/Comp/PriorityAux.ML UNITY/Comp/PriorityAux.thy \
+  UNITY/Comp/Priority.ML UNITY/Comp/Priority.thy \
+  UNITY/Comp/TimerArray.ML UNITY/Comp/TimerArray.thy
 	@$(ISATOOL) usedir $(OUT)/HOL UNITY