use with_paths;
authorwenzelm
Mon, 26 Jun 2000 00:00:40 +0200
changeset 9143 6180c29d2db6
parent 9142 d5a841f89e92
child 9144 20a70ef9c320
use with_paths;
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";