# HG changeset patch
# User huffman
# Date 1269322954 25200
# Node ID 9ef9a20cfba13c056c460a9dad815e2a0b1b1abf
# Parent  676c6005ad03f3a8b8314ee1c1dd667eeac28cd9
remove unused syntax for as_pat, lazy_pat

diff -r 676c6005ad03 -r 9ef9a20cfba1 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Mon Mar 22 22:41:41 2010 -0700
+++ b/src/HOLCF/Fixrec.thy	Mon Mar 22 22:42:34 2010 -0700
@@ -419,10 +419,6 @@
 
 subsection {* Wildcards, as-patterns, and lazy patterns *}
 
-syntax
-  "_as_pat" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "\<as>" 10)
-  "_lazy_pat" :: "'a \<Rightarrow> 'a" ("\<lazy> _" [1000] 1000)
-
 definition
   wild_pat :: "'a \<rightarrow> unit maybe" where
   "wild_pat = (\<Lambda> x. return\<cdot>())"
@@ -438,24 +434,14 @@
 text {* Parse translations (patterns) *}
 translations
   "_pat _" => "CONST wild_pat"
-  "_pat (_as_pat x y)" => "CONST as_pat (_pat y)"
-  "_pat (_lazy_pat x)" => "CONST lazy_pat (_pat x)"
 
 text {* Parse translations (variables) *}
 translations
   "_variable _ r" => "_variable _noargs r"
-  "_variable (_as_pat x y) r" => "_variable (_args x y) r"
-  "_variable (_lazy_pat x) r" => "_variable x r"
 
 text {* Print translations *}
 translations
   "_" <= "_match (CONST wild_pat) _noargs"
-  "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_variable x) v)"
-  "_lazy_pat (_match p v)" <= "_match (CONST lazy_pat p) v"
-
-text {* Lazy patterns in lambda abstractions *}
-translations
-  "_cabs (_lazy_pat p) r" == "CONST Fixrec.cases oo (_Case1 (_lazy_pat p) r)"
 
 lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
 by (simp add: branch_def wild_pat_def)