# HG changeset patch
# User oheimb
# Date 963584929 -7200
# Node ID 40bab6613000ba2f75b6a79ef35254bb2216270e
# Parent  9666f78ecfab2b0a75f9cb63ab62e08dc7403148
tuned syntax

diff -r 9666f78ecfab -r 40bab6613000 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jul 14 16:27:45 2000 +0200
+++ b/src/HOL/List.thy	Fri Jul 14 16:28:49 2000 +0200
@@ -43,7 +43,7 @@
   "@list"     :: args => 'a list                          ("[(_)]")
 
   (* Special syntax for filter *)
-  "@filter"   :: [pttrn, 'a list, bool] => 'a list        ("(1[_:_ ./ _])")
+  "@filter"   :: [pttrn, 'a list, bool] => 'a list        ("(1[_:_./ _])")
 
   (* list update *)
   "_lupdbind"      :: ['a, 'a] => lupdbind            ("(2_ :=/ _)")
diff -r 9666f78ecfab -r 40bab6613000 src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Fri Jul 14 16:27:45 2000 +0200
+++ b/src/HOL/Prod.thy	Fri Jul 14 16:28:49 2000 +0200
@@ -49,10 +49,9 @@
 
 syntax
   "@Tuple"      :: "['a, args] => 'a * 'b"       ("(1'(_,/ _'))")
-
-  "_pattern"    :: [pttrn, patterns] => pttrn    ("'(_,/_')")
-  ""            :: pttrn => patterns             ("_")
-  "_patterns"   :: [pttrn, patterns] => patterns ("_,/_")
+  "_pattern"    :: [pttrn, patterns] => pttrn      ("'(_,/ _')")
+  ""            :: pttrn => patterns                     ("_")
+  "_patterns"   :: [pttrn, patterns] => patterns     ("_,/ _")
 
   "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
   "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    (infixr "<*>" 80)