--- 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";