diff -r 69d815b0e1eb -r 21291189b51e ex/InSort.thy
--- a/ex/InSort.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/InSort.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -14,9 +14,9 @@
 
 rules
   ins_Nil  "ins(f,x,[]) = [x]"
-  ins_Cons "ins(f,x,Cons(y,ys)) =   \
-\	       if(f(x,y), Cons(x,Cons(y,ys)), Cons(y, ins(f,x,ys)))"
+  ins_Cons "ins(f,x,y#ys) =   \
+\	       if(f(x,y), x#y#ys, y# ins(f,x,ys))"
 
   insort_Nil  "insort(f,[]) = []"
-  insort_Cons "insort(f,Cons(x,xs)) = ins(f,x,insort(f,xs))"
+  insort_Cons "insort(f,x#xs) = ins(f,x,insort(f,xs))"
 end