diff -r ea8a1fc512e6 -r 6df4488339e4 src/HOL/Auth/DB-ROOT.ML
--- a/src/HOL/Auth/DB-ROOT.ML	Thu Dec 05 19:01:49 1996 +0100
+++ b/src/HOL/Auth/DB-ROOT.ML	Thu Dec 05 19:03:08 1996 +0100
@@ -20,5 +20,5 @@
   let val thm = normalize_thm [RSspec,RSmp] (result())
   in bind_thm(name, thm) end;
 
-use_thy "Shared";
+use_thy "Message";