# HG changeset patch
# User huffman
# Date 1294514289 28800
# Node ID 655f583840d02671e0fa57ebb4bf7a0021d4cc6c
# Parent  18500bd1f47b2e4c7960b120b0a7e6f62a69aa2e
use proper syntactic types for 'syntax' commands

diff -r 18500bd1f47b -r 655f583840d0 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Sat Jan 08 10:02:43 2011 -0800
+++ b/src/HOL/HOLCF/Cfun.thy	Sat Jan 08 11:18:09 2011 -0800
@@ -30,7 +30,7 @@
 
 subsection {* Syntax for continuous lambda abstraction *}
 
-syntax "_cabs" :: "'a"
+syntax "_cabs" :: "[logic, logic] \<Rightarrow> logic"
 
 parse_translation {*
 (* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
@@ -46,10 +46,10 @@
 text {* Syntax for nested abstractions *}
 
 syntax
-  "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic"  ("(3LAM _./ _)" [1000, 10] 10)
+  "_Lambda" :: "[cargs, logic] \<Rightarrow> logic"  ("(3LAM _./ _)" [1000, 10] 10)
 
 syntax (xsymbols)
-  "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
+  "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
 
 parse_ast_translation {*
 (* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
diff -r 18500bd1f47b -r 655f583840d0 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Sat Jan 08 10:02:43 2011 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy	Sat Jan 08 11:18:09 2011 -0800
@@ -181,7 +181,7 @@
   "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
 
 syntax
-  "_convex_pd" :: "args \<Rightarrow> 'a convex_pd" ("{_}\<natural>")
+  "_convex_pd" :: "args \<Rightarrow> logic" ("{_}\<natural>")
 
 translations
   "{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
diff -r 18500bd1f47b -r 655f583840d0 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Sat Jan 08 10:02:43 2011 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy	Sat Jan 08 11:18:09 2011 -0800
@@ -136,7 +136,7 @@
   "xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
 
 syntax
-  "_lower_pd" :: "args \<Rightarrow> 'a lower_pd" ("{_}\<flat>")
+  "_lower_pd" :: "args \<Rightarrow> logic" ("{_}\<flat>")
 
 translations
   "{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
diff -r 18500bd1f47b -r 655f583840d0 src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Sat Jan 08 10:02:43 2011 -0800
+++ b/src/HOL/HOLCF/Sprod.thy	Sat Jan 08 11:18:09 2011 -0800
@@ -44,7 +44,8 @@
   "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
 
 syntax
-  "_stuple" :: "['a, args] => 'a ** 'b"  ("(1'(:_,/ _:'))")
+  "_stuple" :: "[logic, args] \<Rightarrow> logic"  ("(1'(:_,/ _:'))")
+
 translations
   "(:x, y, z:)" == "(:x, (:y, z:):)"
   "(:x, y:)"    == "CONST spair\<cdot>x\<cdot>y"
diff -r 18500bd1f47b -r 655f583840d0 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Sat Jan 08 10:02:43 2011 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy	Sat Jan 08 11:18:09 2011 -0800
@@ -134,7 +134,7 @@
   "xs \<union>\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
 
 syntax
-  "_upper_pd" :: "args \<Rightarrow> 'a upper_pd" ("{_}\<sharp>")
+  "_upper_pd" :: "args \<Rightarrow> logic" ("{_}\<sharp>")
 
 translations
   "{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>"
diff -r 18500bd1f47b -r 655f583840d0 src/HOL/HOLCF/ex/Letrec.thy
--- a/src/HOL/HOLCF/ex/Letrec.thy	Sat Jan 08 10:02:43 2011 -0800
+++ b/src/HOL/HOLCF/ex/Letrec.thy	Sat Jan 08 11:18:09 2011 -0800
@@ -17,12 +17,12 @@
 nonterminal recbinds and recbindt and recbind
 
 syntax
-  "_recbind"  :: "['a, 'a] \<Rightarrow> recbind"               ("(2_ =/ _)" 10)
+  "_recbind"  :: "[logic, logic] \<Rightarrow> recbind"         ("(2_ =/ _)" 10)
   ""          :: "recbind \<Rightarrow> recbindt"               ("_")
   "_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt"   ("_,/ _")
   ""          :: "recbindt \<Rightarrow> recbinds"              ("_")
   "_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds"  ("_;/ _")
-  "_Letrec"   :: "[recbinds, 'a] \<Rightarrow> 'a"      ("(Letrec (_)/ in (_))" 10)
+  "_Letrec"   :: "[recbinds, logic] \<Rightarrow> logic"        ("(Letrec (_)/ in (_))" 10)
 
 translations
   (recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"