# HG changeset patch
# User paulson
# Date 929090060 -7200
# Node ID 852f9ed01a53d64e27703e2d742f516bc118119e
# Parent  a42849eeb67485775267f0bf60c657e5d670e57c
no longer needs ../Lex

diff -r a42849eeb674 -r 852f9ed01a53 src/HOL/UNITY/ROOT.ML
--- a/src/HOL/UNITY/ROOT.ML	Fri Jun 11 10:33:43 1999 +0200
+++ b/src/HOL/UNITY/ROOT.ML	Fri Jun 11 10:34:20 1999 +0200
@@ -9,10 +9,9 @@
 writeln"Root file for HOL/UNITY";
 
 set proof_timing;
+set HOL_quantifiers;
 
-add_path "../Lex";	(*to find Prefix.thy*)
-
-time_use_thy"UNITY";
+time_use_thy "UNITY";
 time_use_thy "Deadlock";
 time_use_thy "WFair";
 time_use_thy "Common";