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