src/ZF/Sum.thy

--- a/src/ZF/Sum.thy	Mon Oct 20 10:53:25 1997 +0200
+++ b/src/ZF/Sum.thy	Mon Oct 20 10:53:42 1997 +0200
@@ -17,7 +17,7 @@
     case        :: [i=>i, i=>i, i]=>i
     Part        :: [i,i=>i] => i
 
-path Sum
+local
 
 defs
     sum_def     "A+B == {0}*A Un {1}*B"