diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Sum.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -14,7 +14,7 @@
     case        :: "[i=>i, i=>i, i]=>i"
     Part        :: "[i,i=>i] => i"
 
-rules
+defs
     sum_def     "A+B == {0}*A Un {1}*B"
     Inl_def     "Inl(a) == <0,a>"
     Inr_def     "Inr(b) == <1,b>"