src/ZF/Coind/Map.thy

--- a/src/ZF/Coind/Map.thy	Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Coind/Map.thy	Thu Jan 07 10:56:05 1999 +0100
@@ -21,7 +21,8 @@
   map_app :: [i,i]=>i
 defs
   map_emp_def "map_emp == 0"
-  map_owr_def "map_owr(m,a,b) == SUM x:{a} Un domain(m).if(x=a,b,m``{x})"
+  map_owr_def "map_owr(m,a,b) ==
+	         SUM x:{a} Un domain(m). if x=a then b else m``{x}"
   map_app_def "map_app(m,a) == m``{a}"
   
 end