src/HOL/Fun.thy
changeset 8258 666d3a4f3b9d
parent 7374 dec7b838f5cb
child 8924 c434283b4cfa
--- 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"