diff -r cbd32a0f2f41 -r 74be52691d62 src/HOLCF/Sprod1.thy
--- a/src/HOLCF/Sprod1.thy	Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/Sprod1.thy	Thu Jun 29 16:28:40 1995 +0200
@@ -11,12 +11,10 @@
 consts
   less_sprod	:: "[('a ** 'b),('a ** 'b)] => bool"	
 
-rules
-
-  less_sprod_def "less_sprod(p1,p2) == @z.
-	 ( p1=Ispair(UU,UU) --> z = True)
-	&(~p1=Ispair(UU,UU) --> z = (   Isfst(p1) << Isfst(p2) &
-					Issnd(p1) << Issnd(p2)))"
+defs
+  less_sprod_def "less_sprod p1 p2 == 
+	if p1 = Ispair UU UU
+		then True
+		else Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
 
 end
-