diff -r 83f908ed3c04 -r 1d5bee4d047f src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Mon Oct 20 10:53:25 1997 +0200
+++ b/src/ZF/OrdQuant.thy	Mon Oct 20 10:53:42 1997 +0200
@@ -32,7 +32,7 @@
   "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
   "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
 
-path OrdQuant
+local
 
 defs