# HG changeset patch
# User wenzelm
# Date 961970440 -7200
# Node ID 6180c29d2db64ae87d9e558d073808274f8cd114
# Parent  d5a841f89e921460285a34300b9155e3f0c0bc3b
use with_paths;

diff -r d5a841f89e92 -r 6180c29d2db6 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Sun Jun 25 23:58:54 2000 +0200
+++ b/src/HOL/MicroJava/ROOT.ML	Mon Jun 26 00:00:40 2000 +0200
@@ -1,8 +1,8 @@
 
-goals_limit:=1;
+goals_limit := 1;
 
 Unify.search_bound := 40;
 Unify.trace_bound  := 40;
 
-with_path "J" (with_path "JVM" (with_path "BV" use_thy)) "JTypeSafe";
-with_path "J" (with_path "JVM" (with_path "BV" use_thy)) "BVSpecTypeSafe";
+with_paths ["J", "JVM", "BV"] use_thy "JTypeSafe";
+with_paths ["J", "JVM", "BV"] use_thy "BVSpecTypeSafe";