--- a/src/ZF/OrderType.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/OrderType.thy Tue Nov 29 00:31:31 1994 +0100
@@ -13,7 +13,7 @@
ordermap :: "[i,i]=>i"
ordertype :: "[i,i]=>i"
-rules
+defs
ordermap_def
"ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"