# HG changeset patch
# User oheimb
# Date 950901856 -3600
# Node ID 666d3a4f3b9dcee3fd4a2fddfae5ec75787d23c9
# Parent  fe9bf28e8a584a533c4ad8cd65174959d10230bd
changed precedence of function update

diff -r fe9bf28e8a58 -r 666d3a4f3b9d src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Feb 18 18:29:28 2000 +0100
+++ b/src/HOL/Fun.ML	Fri Feb 18 20:24:16 2000 +0100
@@ -420,7 +420,7 @@
 qed "fun_upd_upd";
 Addsimps [fun_upd_upd];
 
-Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
+Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)";
 by (rtac ext 1);
 by Auto_tac;
 qed "fun_upd_twist";
diff -r fe9bf28e8a58 -r 666d3a4f3b9d src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Feb 18 18:29:28 2000 +0100
+++ b/src/HOL/Fun.thy	Fri Feb 18 20:24:16 2000 +0100
@@ -23,7 +23,7 @@
   "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
   ""               :: updbind => updbinds             ("_")
   "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
-  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
+  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [1000,0] 900)
 
 translations
   "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"