diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/ROOT.ML --- a/src/HOL/MicroJava/ROOT.ML Thu Feb 01 20:51:48 2001 +0100 +++ b/src/HOL/MicroJava/ROOT.ML Thu Feb 01 20:53:13 2001 +0100 @@ -1,9 +1,6 @@ goals_limit := 1; -Unify.search_bound := 40; -Unify.trace_bound := 40; - add_path "J"; add_path "JVM"; add_path "BV";