# HG changeset patch
# User oheimb
# Date 976125950 -3600
# Node ID e460c53c1c9b9722f87fda491625b36709e20cc2
# Parent  1dc640d06d19611c99ceeb94cb971d81feb712aa
simplified interactive handling

diff -r 1dc640d06d19 -r e460c53c1c9b src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Wed Dec 06 17:03:26 2000 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Wed Dec 06 19:05:50 2000 +0100
@@ -4,4 +4,7 @@
 Unify.search_bound := 40;
 Unify.trace_bound  := 40;
 
-with_paths ["J", "JVM", "BV"] use_thy "Digest"; 
+add_path "J";
+add_path "JVM";
+add_path "BV";
+use_thy "Digest";