# HG changeset patch
# User wenzelm
# Date 961970307 -7200
# Node ID 49f6e45e7199be2e92ed57d52ed5fb16063f6da7
# Parent  69e8938c24090675d6756a0bdeaf6a423c7e7b1d
tuned;

diff -r 69e8938c2409 -r 49f6e45e7199 src/HOL/Fun.thy
--- 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 ("_,/ _")