# HG changeset patch
# User huffman
# Date 1131387833 -3600
# Node ID 08ec4f1f116dbe2930cb7703b730b16ad6e6326f
# Parent  94b528311e22e7993f605af2993b573345cdd664
remove syntax for as-patterns

diff -r 94b528311e22 -r 08ec4f1f116d src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Mon Nov 07 19:03:02 2005 +0100
+++ b/src/HOLCF/Fixrec.thy	Mon Nov 07 19:23:53 2005 +0100
@@ -171,7 +171,7 @@
   "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ =>/ _)" 10)
   ""            :: "Case_syn => Cases_syn"               ("_")
   "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  ("_/ | _")
-  "_as_pattern" :: "[idt, 'a] \<Rightarrow> 'a"                     (infixr "as" 10)
+  "_as_pattern" :: "[idt, 'a] \<Rightarrow> 'a"                     (* infixr "as" 10 *)
 
 syntax (xsymbols)
   "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)