Digest.thy as toplevel theory

--- a/src/HOL/MicroJava/ROOT.ML	Thu Sep 21 12:25:07 2000 +0200
+++ b/src/HOL/MicroJava/ROOT.ML	Thu Sep 21 12:25:48 2000 +0200
@@ -4,8 +4,4 @@
 Unify.search_bound := 40;
 Unify.trace_bound  := 40;
 
-with_paths ["J"             ] use_thy "JTypeSafe";
-with_paths ["J"             ] use_thy "Example";
-with_paths ["J", "JVM", "BV"] use_thy "BVSpecTypeSafe";
-with_paths ["J", "JVM", "BV"] use_thy "LBVCorrect";
-with_paths ["J", "JVM", "BV"] use_thy "LBVComplete";
+with_paths ["J", "JVM", "BV"] use_thy "Digest";