src/ZF/Sum.thy

--- a/src/ZF/Sum.thy	Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/Sum.thy	Wed Aug 18 12:19:27 2010 +0200
@@ -9,8 +9,6 @@
 
 text{*And the "Part" primitive for simultaneous recursive type definitions*}
 
-global
-
 definition sum :: "[i,i]=>i" (infixr "+" 65) where
      "A+B == {0}*A Un {1}*B"
 
@@ -27,8 +25,6 @@
 definition Part :: "[i,i=>i] => i" where
      "Part(A,h) == {x: A. EX z. x = h(z)}"
 
-local
-
 subsection{*Rules for the @{term Part} Primitive*}
 
 lemma Part_iff: