diff -r 23b7e14ce640 -r a8c9ed3f9818 src/HOL/Auth/ROOT.ML
--- a/src/HOL/Auth/ROOT.ML	Wed Sep 14 23:06:02 2005 +0200
+++ b/src/HOL/Auth/ROOT.ML	Wed Sep 14 23:14:57 2005 +0200
@@ -8,6 +8,8 @@
 
 no_document use_thy "NatPair";
 
+add_path "Guard";
+
 set timing;
 
 (*Shared-key protocols*)
@@ -31,9 +33,9 @@
 time_use_thy "CertifiedEmail";
 
 (*Blanqui's "guard" concept: protocol-independent secrecy*)
-time_use_thy "Guard/P1";
-time_use_thy "Guard/P2";
-time_use_thy "Guard/NS_Public";
-time_use_thy "Guard/OtwayRees";
-time_use_thy "Guard/Yahalom";
-time_use_thy "Guard/Proto";
+time_use_thy "P1";
+time_use_thy "P2";
+time_use_thy "Guard_NS_Public";
+time_use_thy "Guard_OtwayRees";
+time_use_thy "Guard_Yahalom";
+time_use_thy "Proto";