# HG changeset patch
# User clasohm
# Date 750344302 -3600
# Node ID 37e93ef9c756f6fac7a109d6c7d10278f4abbcdc
# Parent  c78503b345c4f7f3309c41338baad5d5c67fdc47
renamed ordinal.* to ord.*

diff -r c78503b345c4 -r 37e93ef9c756 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Mon Oct 11 12:35:00 1993 +0100
+++ b/src/ZF/ROOT.ML	Mon Oct 11 13:58:22 1993 +0100
@@ -54,7 +54,7 @@
 use_thy "perm";
 use_thy "trancl";
 use_thy "wf";
-use_thy "ordinal";
+use_thy "ord";
 use_thy "nat";
 use_thy "epsilon";
 use_thy "arith";