--- a/src/HOL/Fun.thy Sun Jun 25 23:57:29 2000 +0200
+++ b/src/HOL/Fun.thy Sun Jun 25 23:58:27 2000 +0200
@@ -10,16 +10,12 @@
instance set :: (term) order
(subset_refl,subset_trans,subset_antisym,psubset_eq)
-nonterminals
- updbinds updbind
-
consts
fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+nonterminals
+ updbinds updbind
syntax
-
- (* Let expressions *)
-
"_updbind" :: ['a, 'a] => updbind ("(2_ :=/ _)")
"" :: updbind => updbinds ("_")
"_updbinds" :: [updbind, updbinds] => updbinds ("_,/ _")