--- a/ex/sorting.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/sorting.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -18,13 +18,13 @@
 
 sorted1_Nil  "sorted1(f,[])"
 sorted1_One  "sorted1(f,[x])"
-sorted1_Cons "sorted1(f,Cons(x,Cons(y,zs))) = (f(x,y) & sorted1(f,Cons(y,zs)))"
+sorted1_Cons "sorted1(f,Cons(x,y#zs)) = (f(x,y) & sorted1(f,y#zs))"
 
 sorted_Nil "sorted(le,[])"
-sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
+sorted_Cons "sorted(le,x#xs) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
 
 mset_Nil "mset([],y) = 0"
-mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
+mset_Cons "mset(x#xs,y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
 
 total_def  "total(r) == (!x y. r(x,y) | r(y,x))"
 transf_def "transf(f) == (!x y z. f(x,y) & f(y,z) --> f(x,z))"