src/ZF/List.ML

--- a/src/ZF/List.ML	Tue Oct 05 17:49:23 1993 +0100
+++ b/src/ZF/List.ML	Wed Oct 06 09:58:53 1993 +0100
@@ -67,11 +67,11 @@
 
 (** For recursion **)
 
-goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
+goalw List.thy List.con_defs "rank(a) < rank(Cons(a,l))";
 by (simp_tac rank_ss 1);
 val rank_Cons1 = result();
 
-goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
+goalw List.thy List.con_defs "rank(l) < rank(Cons(a,l))";
 by (simp_tac rank_ss 1);
 val rank_Cons2 = result();