# HG changeset patch
# User clasohm
# Date 817815793 -3600
# Node ID 92f83b9d17e1a8b90b32557ba7144208da0ae1e0
# Parent  d04af07266e8896159509a3a48c2bdac7ed549f6
removed quotes from consts and syntax sections

diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/ABP/Abschannel.thy
--- a/src/HOL/IOA/ABP/Abschannel.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Abschannel.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -14,21 +14,21 @@
 
 consts
  
-ch_asig  :: "'a act signature"
-ch_trans :: "('a act, 'a list)transition set"
-ch_ioa   :: "('a act, 'a list)ioa"
+ch_asig  :: 'a act signature
+ch_trans :: ('a act, 'a list)transition set
+ch_ioa   :: ('a act, 'a list)ioa
 
-rsch_actions  :: "'m action => bool act option"
+rsch_actions  :: 'm action => bool act option
 srch_actions  :: "'m action =>(bool * 'm) act option"
 
 srch_asig, 
-rsch_asig  :: "'m action signature"
+rsch_asig  :: 'm action signature
 
-srch_trans :: "('m action, 'm packet list)transition set"
-rsch_trans :: "('m action, bool list)transition set"
+srch_trans :: ('m action, 'm packet list)transition set
+rsch_trans :: ('m action, bool list)transition set
 
-srch_ioa   :: "('m action, 'm packet list)ioa"
-rsch_ioa   :: "('m action, bool list)ioa"   
+srch_ioa   :: ('m action, 'm packet list)ioa
+rsch_ioa   :: ('m action, bool list)ioa   
 
 
 defs
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/ABP/Abschannel_finite.thy
--- a/src/HOL/IOA/ABP/Abschannel_finite.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Abschannel_finite.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -10,22 +10,22 @@
  
 consts
  
-ch_fin_asig  :: "'a act signature"
+ch_fin_asig  :: 'a act signature
 
-ch_fin_trans :: "('a act, 'a list)transition set"
+ch_fin_trans :: ('a act, 'a list)transition set
 
-ch_fin_ioa   :: "('a act, 'a list)ioa"
+ch_fin_ioa   :: ('a act, 'a list)ioa
 
 srch_fin_asig, 
-rsch_fin_asig  :: "'m action signature"
+rsch_fin_asig  :: 'm action signature
 
-srch_fin_trans :: "('m action, 'm packet list)transition set"
-rsch_fin_trans :: "('m action, bool list)transition set"
+srch_fin_trans :: ('m action, 'm packet list)transition set
+rsch_fin_trans :: ('m action, bool list)transition set
 
-srch_fin_ioa   :: "('m action, 'm packet list)ioa"
-rsch_fin_ioa   :: "('m action, bool list)ioa"   
+srch_fin_ioa   :: ('m action, 'm packet list)ioa
+rsch_fin_ioa   :: ('m action, bool list)ioa   
 
-reverse        :: "'a list => 'a list"
+reverse        :: 'a list => 'a list
 
 primrec
   reverse List.list  
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/ABP/Correctness.thy
--- a/src/HOL/IOA/ABP/Correctness.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Correctness.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -10,9 +10,9 @@
 
 consts
 
-reduce           :: "'a list => 'a list"
+reduce           :: 'a list => 'a list
 
-abs              :: "'c"
+abs              :: 'c
 system_ioa       :: "('m action, bool * 'm impl_state)ioa"
 system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"
   
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/ABP/Env.thy
--- a/src/HOL/IOA/ABP/Env.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Env.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -16,10 +16,10 @@
 
 consts
 
-env_asig   :: "'m action signature"
-env_trans  :: "('m action, 'm env_state)transition set"
-env_ioa    :: "('m action, 'm env_state)ioa"
-next       :: "'m env_state => bool"
+env_asig   :: 'm action signature
+env_trans  :: ('m action, 'm env_state)transition set
+env_ioa    :: ('m action, 'm env_state)ioa
+next       :: 'm env_state => bool
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/ABP/Impl.thy
--- a/src/HOL/IOA/ABP/Impl.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Impl.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -16,11 +16,11 @@
 
 
 consts
- impl_ioa    :: "('m action, 'm impl_state)ioa"
- sen         :: "'m impl_state => 'm sender_state"
- rec         :: "'m impl_state => 'm receiver_state"
- srch        :: "'m impl_state => 'm packet list"
- rsch        :: "'m impl_state => bool list"
+ impl_ioa    :: ('m action, 'm impl_state)ioa
+ sen         :: 'm impl_state => 'm sender_state
+ rec         :: 'm impl_state => 'm receiver_state
+ srch        :: 'm impl_state => 'm packet list
+ rsch        :: 'm impl_state => bool list
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/ABP/Impl_finite.thy
--- a/src/HOL/IOA/ABP/Impl_finite.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Impl_finite.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -16,11 +16,11 @@
 
 consts
 
- impl_fin_ioa    :: "('m action, 'm impl_fin_state)ioa"
- sen_fin         :: "'m impl_fin_state => 'm sender_state"
- rec_fin         :: "'m impl_fin_state => 'm receiver_state"
- srch_fin        :: "'m impl_fin_state => 'm packet list"
- rsch_fin        :: "'m impl_fin_state => bool list"
+ impl_fin_ioa    :: ('m action, 'm impl_fin_state)ioa
+ sen_fin         :: 'm impl_fin_state => 'm sender_state
+ rec_fin         :: 'm impl_fin_state => 'm receiver_state
+ srch_fin        :: 'm impl_fin_state => 'm packet list
+ rsch_fin        :: 'm impl_fin_state => bool list
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/ABP/Packet.thy
--- a/src/HOL/IOA/ABP/Packet.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Packet.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -14,8 +14,8 @@
 
 consts
 
-  hdr  :: "'msg packet => bool"
-  msg :: "'msg packet => 'msg"
+  hdr  :: 'msg packet => bool
+  msg :: 'msg packet => 'msg
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/ABP/Receiver.thy
--- a/src/HOL/IOA/ABP/Receiver.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Receiver.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -16,11 +16,11 @@
 
 consts
 
-  receiver_asig :: "'m action signature"
-  receiver_trans:: "('m action, 'm receiver_state)transition set"
-  receiver_ioa  :: "('m action, 'm receiver_state)ioa"
-  rq            :: "'m receiver_state => 'm list"
-  rbit          :: "'m receiver_state => bool"
+  receiver_asig :: 'm action signature
+  receiver_trans:: ('m action, 'm receiver_state)transition set
+  receiver_ioa  :: ('m action, 'm receiver_state)ioa
+  rq            :: 'm receiver_state => 'm list
+  rbit          :: 'm receiver_state => bool
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/ABP/Sender.thy
--- a/src/HOL/IOA/ABP/Sender.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Sender.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -15,11 +15,11 @@
 
 consts
 
-sender_asig   :: "'m action signature"
-sender_trans  :: "('m action, 'm sender_state)transition set"
-sender_ioa    :: "('m action, 'm sender_state)ioa"
-sq            :: "'m sender_state => 'm list"
-sbit          :: "'m sender_state => bool"
+sender_asig   :: 'm action signature
+sender_trans  :: ('m action, 'm sender_state)transition set
+sender_ioa    :: ('m action, 'm sender_state)ioa
+sq            :: 'm sender_state => 'm list
+sbit          :: 'm sender_state => bool
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/ABP/Spec.thy
--- a/src/HOL/IOA/ABP/Spec.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Spec.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -10,9 +10,9 @@
 
 consts
 
-spec_sig   :: "'m action signature"
-spec_trans :: "('m action, 'm list)transition set"
-spec_ioa   :: "('m action, 'm list)ioa"
+spec_sig   :: 'm action signature
+spec_trans :: ('m action, 'm list)transition set
+spec_ioa   :: ('m action, 'm list)ioa
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/NTP/Abschannel.thy
--- a/src/HOL/IOA/NTP/Abschannel.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Abschannel.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -12,23 +12,23 @@
 
 consts
  
-ch_asig  :: "'a act signature"
+ch_asig  :: 'a act signature
 
-ch_trans :: "('a act, 'a multiset)transition set"
+ch_trans :: ('a act, 'a multiset)transition set
 
-ch_ioa   :: "('a act, 'a multiset)ioa"
+ch_ioa   :: ('a act, 'a multiset)ioa
 
-rsch_actions  :: "'m action => bool act option"
+rsch_actions  :: 'm action => bool act option
 srch_actions  :: "'m action =>(bool * 'm) act option"
 
 srch_asig, 
-rsch_asig  :: "'m action signature"
+rsch_asig  :: 'm action signature
 
-srch_trans :: "('m action, 'm packet multiset)transition set"
-rsch_trans :: "('m action, bool multiset)transition set"
+srch_trans :: ('m action, 'm packet multiset)transition set
+rsch_trans :: ('m action, bool multiset)transition set
 
-srch_ioa   :: "('m action, 'm packet multiset)ioa"
-rsch_ioa   :: "('m action, bool multiset)ioa"   
+srch_ioa   :: ('m action, 'm packet multiset)ioa
+rsch_ioa   :: ('m action, bool multiset)ioa   
 
 
 defs
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/NTP/Correctness.thy
--- a/src/HOL/IOA/NTP/Correctness.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Correctness.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -10,7 +10,7 @@
 
 consts
 
-hom :: "'m impl_state => 'm list"
+hom :: 'm impl_state => 'm list
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/NTP/Impl.thy
--- a/src/HOL/IOA/NTP/Impl.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Impl.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -16,14 +16,14 @@
 
 
 consts
- impl_ioa    :: "('m action, 'm impl_state)ioa"
- sen         :: "'m impl_state => 'm sender_state"
- rec         :: "'m impl_state => 'm receiver_state"
- srch        :: "'m impl_state => 'm packet multiset"
- rsch        :: "'m impl_state => bool multiset"
+ impl_ioa    :: ('m action, 'm impl_state)ioa
+ sen         :: 'm impl_state => 'm sender_state
+ rec         :: 'm impl_state => 'm receiver_state
+ srch        :: 'm impl_state => 'm packet multiset
+ rsch        :: 'm impl_state => bool multiset
  inv1, inv2, 
- inv3, inv4  :: "'m impl_state => bool"
- hdr_sum     :: "'m packet multiset => bool => nat"
+ inv3, inv4  :: 'm impl_state => bool
+ hdr_sum     :: 'm packet multiset => bool => nat
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/NTP/Multiset.thy
--- a/src/HOL/IOA/NTP/Multiset.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Multiset.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -19,11 +19,11 @@
 
 consts
 
-  "{|}"  :: "'a multiset"                        ("{|}")
-  addm   :: "['a multiset, 'a] => 'a multiset"
-  delm   :: "['a multiset, 'a] => 'a multiset"
-  countm :: "['a multiset, 'a => bool] => nat"
-  count  :: "['a multiset, 'a] => nat"
+  "{|}"  :: 'a multiset                        ("{|}")
+  addm   :: ['a multiset, 'a] => 'a multiset
+  delm   :: ['a multiset, 'a] => 'a multiset
+  countm :: ['a multiset, 'a => bool] => nat
+  count  :: ['a multiset, 'a] => nat
 
 rules
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/NTP/Packet.thy
--- a/src/HOL/IOA/NTP/Packet.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Packet.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -14,8 +14,8 @@
 
 consts
 
-  hdr  :: "'msg packet => bool"
-  msg :: "'msg packet => 'msg"
+  hdr  :: 'msg packet => bool
+  msg :: 'msg packet => 'msg
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/NTP/Receiver.thy
--- a/src/HOL/IOA/NTP/Receiver.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Receiver.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -16,14 +16,14 @@
 
 consts
 
-  receiver_asig :: "'m action signature"
-  receiver_trans:: "('m action, 'm receiver_state)transition set"
-  receiver_ioa  :: "('m action, 'm receiver_state)ioa"
-  rq            :: "'m receiver_state => 'm list"
-  rsent         :: "'m receiver_state => bool multiset"
-  rrcvd         :: "'m receiver_state => 'm packet multiset"
-  rbit          :: "'m receiver_state => bool"
-  rsending      :: "'m receiver_state => bool"
+  receiver_asig :: 'm action signature
+  receiver_trans:: ('m action, 'm receiver_state)transition set
+  receiver_ioa  :: ('m action, 'm receiver_state)ioa
+  rq            :: 'm receiver_state => 'm list
+  rsent         :: 'm receiver_state => bool multiset
+  rrcvd         :: 'm receiver_state => 'm packet multiset
+  rbit          :: 'm receiver_state => bool
+  rsending      :: 'm receiver_state => bool
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/NTP/Sender.thy
--- a/src/HOL/IOA/NTP/Sender.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Sender.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -15,13 +15,13 @@
 
 consts
 
-sender_asig   :: "'m action signature"
-sender_trans  :: "('m action, 'm sender_state)transition set"
-sender_ioa    :: "('m action, 'm sender_state)ioa"
-sq            :: "'m sender_state => 'm list"
-ssent,srcvd   :: "'m sender_state => bool multiset"
-sbit          :: "'m sender_state => bool"
-ssending      :: "'m sender_state => bool"
+sender_asig   :: 'm action signature
+sender_trans  :: ('m action, 'm sender_state)transition set
+sender_ioa    :: ('m action, 'm sender_state)ioa
+sq            :: 'm sender_state => 'm list
+ssent,srcvd   :: 'm sender_state => bool multiset
+sbit          :: 'm sender_state => bool
+ssending      :: 'm sender_state => bool
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/IOA/NTP/Spec.thy
--- a/src/HOL/IOA/NTP/Spec.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Spec.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -10,9 +10,9 @@
 
 consts
 
-spec_sig   :: "'m action signature"
-spec_trans :: "('m action, 'm list)transition set"
-spec_ioa   :: "('m action, 'm list)ioa"
+spec_sig   :: 'm action signature
+spec_trans :: ('m action, 'm list)transition set
+spec_ioa   :: ('m action, 'm list)ioa
 
 defs
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/Lambda/Eta.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -7,11 +7,11 @@
 *)
 
 Eta = ParRed + Commutation +
-consts free :: "db => nat => bool"
-       decr :: "[db,nat] => db"
+consts free :: db => nat => bool
+       decr :: [db,nat] => db
        eta  :: "(db * db) set"
 
-syntax  "-e>", "-e>>", "-e>=" , "->=" :: "[db,db] => bool" (infixl 50)
+syntax  "-e>", "-e>>", "-e>=" , "->=" :: [db,db] => bool (infixl 50)
 
 translations
   "s -e>  t" == "(s,t) : eta"
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -12,11 +12,11 @@
 datatype db = Var nat | "@" db db (infixl 200) | Fun db
 
 consts
-  subst  :: "[db,db,nat]=>db" ("_[_'/_]" [300,0,0] 300)
-  lift   :: "[db,nat] => db"
+  subst  :: [db,db,nat]=>db ("_[_'/_]" [300,0,0] 300)
+  lift   :: [db,nat] => db
   (* optimized versions *)
-  substn :: "[db,db,nat] => db"
-  liftn  :: "[nat,db,nat] => db"
+  substn :: [db,db,nat] => db
+  liftn  :: [nat,db,nat] => db
 
 primrec lift db
   lift_Var "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
@@ -42,7 +42,7 @@
 
 consts  beta :: "(db * db) set"
 
-syntax  "->", "->>" :: "[db,db] => bool" (infixl 50)
+syntax  "->", "->>" :: [db,db] => bool (infixl 50)
 
 translations
   "s -> t"  == "(s,t) : beta"
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/Lambda/ParRed.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -10,7 +10,7 @@
 
 consts  par_beta :: "(db * db) set"
 
-syntax  "=>" :: "[db,db] => bool" (infixl 50)
+syntax  "=>" :: [db,db] => bool (infixl 50)
 
 translations
   "s => t" == "(s,t) : par_beta"
@@ -23,8 +23,8 @@
     beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
 
 consts
-  cd  :: "db => db"
-  deFun :: "db => db"
+  cd  :: db => db
+  deFun :: db => db
 
 primrec cd db
   cd_Var "cd(Var n) = Var n"
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/MiniML/I.thy
--- a/src/HOL/MiniML/I.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/MiniML/I.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -8,7 +8,7 @@
 I = W +
 
 consts
-	I :: "[expr, type_expr list, nat, subst] => result_W"
+	I :: [expr, type_expr list, nat, subst] => result_W
 
 primrec I expr
         I_Var	"I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/MiniML/Maybe.thy
--- a/src/HOL/MiniML/Maybe.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/MiniML/Maybe.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -10,7 +10,7 @@
 
 datatype 'a maybe =  Ok 'a | Fail
 
-consts bind :: "['a maybe, 'a => 'b maybe] => 'b maybe" (infixl 60)
+consts bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
 
 defs
   bind_def "m bind f == case m of Ok r => f r | Fail => Fail"
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/MiniML/MiniML.thy
--- a/src/HOL/MiniML/MiniML.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/MiniML/MiniML.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -16,7 +16,7 @@
 consts
 	has_type :: "(type_expr list * expr * type_expr)set"
 syntax
-        "@has_type" :: "[type_expr list, expr, type_expr] => bool"
+        "@has_type" :: [type_expr list, expr, type_expr] => bool
                        ("((_) |-/ (_) :: (_))" 60)
 translations 
         "a |- e :: t" == "(a,e,t):has_type"
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/MiniML/Type.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -29,13 +29,13 @@
 
 (* identity *)
 consts
-	id_subst :: "subst"
+	id_subst :: subst
 defs
 	id_subst_def "id_subst == (%n.TVar n)"
 
 (* extension of substitution to type structures *)
 consts
-	app_subst :: "[subst, 'a::type_struct] => 'a::type_struct" ("$")
+	app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
 
 rules
 	app_subst_TVar  "$ s (TVar n) = s n" 
@@ -45,7 +45,7 @@
   
 (* free_tv s: the type variables occuring freely in the type structure s *)
 consts
-	free_tv :: "['a::type_struct] => nat set"
+	free_tv :: ['a::type_struct] => nat set
 
 rules
 	free_tv_TVar	"free_tv (TVar m) = {m}"
@@ -55,13 +55,13 @@
 
 (* domain of a substitution *)
 consts
-	dom :: "subst => nat set"
+	dom :: subst => nat set
 defs
 	dom_def 	"dom s == {n. s n ~= TVar n}" 
 
 (* codomain of a substitutions: the introduced variables *)
 consts
-     cod :: "subst => nat set"
+     cod :: subst => nat set
 defs
 	cod_def		"cod s == (UN m:dom s. free_tv (s m))"
 
@@ -72,13 +72,13 @@
    structure s, i.e. whether n is greater than any type variable 
    occuring in the type structure *)
 consts
-	new_tv :: "[nat,'a::type_struct] => bool"
+	new_tv :: [nat,'a::type_struct] => bool
 defs
         new_tv_def      "new_tv n ts == ! m. m:free_tv ts --> m<n"
 
 (* unification algorithm mgu *)
 consts
-	mgu :: "[type_expr,type_expr] => subst maybe"
+	mgu :: [type_expr,type_expr] => subst maybe
 rules
 	mgu_eq 	 "mgu t1 t2 = Ok u ==> $ u t1 = $ u t2"
 	mgu_mg 	 "[| (mgu t1 t2) = Ok u; $ s t1 = $ s t2 |] ==>
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/MiniML/W.thy
--- a/src/HOL/MiniML/W.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/MiniML/W.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -13,7 +13,7 @@
 
 (* type inference algorithm W *)
 consts
-	W :: "[expr, type_expr list, nat] => result_W"
+	W :: [expr, type_expr list, nat] => result_W
 
 primrec W expr
   W_Var	"W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/BT.thy
--- a/src/HOL/ex/BT.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/BT.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -11,13 +11,13 @@
 datatype 'a bt = Lf  |  Br 'a ('a bt) ('a bt)
   
 consts
-    n_nodes	:: "'a bt => nat"
-    n_leaves   	:: "'a bt => nat"
-    reflect 	:: "'a bt => 'a bt"
-    bt_map      :: "('a=>'b) => ('a bt => 'b bt)"
-    preorder    :: "'a bt => 'a list"
-    inorder     :: "'a bt => 'a list"
-    postorder   :: "'a bt => 'a list"
+    n_nodes	:: 'a bt => nat
+    n_leaves   	:: 'a bt => nat
+    reflect 	:: 'a bt => 'a bt
+    bt_map      :: ('a=>'b) => ('a bt => 'b bt)
+    preorder    :: 'a bt => 'a list
+    inorder     :: 'a bt => 'a list
+    postorder   :: 'a bt => 'a list
 
 primrec n_nodes bt
   n_nodes_Lf "n_nodes (Lf) = 0"
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/InSort.thy
--- a/src/HOL/ex/InSort.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/InSort.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -9,8 +9,8 @@
 InSort  =  Sorting +
 
 consts
-  ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list"
-  insort :: "[['a,'a]=>bool, 'a list] => 'a list"
+  ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list
+  insort :: [['a,'a]=>bool, 'a list] => 'a list
 
 primrec ins List.list
   ins_Nil  "ins f x [] = [x]"
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/LList.thy
--- a/src/HOL/ex/LList.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/LList.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -32,34 +32,34 @@
    llist :: (term)term
 
 consts
-  list_Fun   :: "['a item set, 'a item set] => 'a item set"
+  list_Fun   :: ['a item set, 'a item set] => 'a item set
   LListD_Fun :: 
       "[('a item * 'a item)set, ('a item * 'a item)set] => 
       ('a item * 'a item)set"
 
-  llist      :: "'a item set => 'a item set"
+  llist      :: 'a item set => 'a item set
   LListD     :: "('a item * 'a item)set => ('a item * 'a item)set"
   llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
 
-  Rep_llist  :: "'a llist => 'a item"
-  Abs_llist  :: "'a item => 'a llist"
-  LNil       :: "'a llist"
-  LCons      :: "['a, 'a llist] => 'a llist"
+  Rep_llist  :: 'a llist => 'a item
+  Abs_llist  :: 'a item => 'a llist
+  LNil       :: 'a llist
+  LCons      :: ['a, 'a llist] => 'a llist
   
-  llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
+  llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
 
   LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
   LList_corec     :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
   llist_corec     :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
 
-  Lmap	     :: "('a item => 'b item) => ('a item => 'b item)"
-  lmap	     :: "('a=>'b) => ('a llist => 'b llist)"
+  Lmap	     :: ('a item => 'b item) => ('a item => 'b item)
+  lmap	     :: ('a=>'b) => ('a llist => 'b llist)
 
-  iterates   :: "['a => 'a, 'a] => 'a llist"
+  iterates   :: ['a => 'a, 'a] => 'a llist
 
-  Lconst     :: "'a item => 'a item"
-  Lappend    :: "['a item, 'a item] => 'a item"
-  lappend    :: "['a llist, 'a llist] => 'a llist"
+  Lconst     :: 'a item => 'a item
+  Lappend    :: ['a item, 'a item] => 'a item
+  lappend    :: ['a llist, 'a llist] => 'a llist
 
 
 coinductive "llist(A)"
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/MT.thy
--- a/src/HOL/ex/MT.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/MT.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -46,48 +46,48 @@
   TyEnv :: term
 
 consts
-  c_app :: "[Const, Const] => Const"
+  c_app :: [Const, Const] => Const
 
-  e_const :: "Const => Ex"
-  e_var :: "ExVar => Ex"
-  e_fn :: "[ExVar, Ex] => Ex" ("fn _ => _" [0,51] 1000)
-  e_fix :: "[ExVar, ExVar, Ex] => Ex" ("fix _ ( _ ) = _" [0,51,51] 1000)
-  e_app :: "[Ex, Ex] => Ex" ("_ @ _" [51,51] 1000)
-  e_const_fst :: "Ex => Const"
+  e_const :: Const => Ex
+  e_var :: ExVar => Ex
+  e_fn :: [ExVar, Ex] => Ex ("fn _ => _" [0,51] 1000)
+  e_fix :: [ExVar, ExVar, Ex] => Ex ("fix _ ( _ ) = _" [0,51,51] 1000)
+  e_app :: [Ex, Ex] => Ex ("_ @ _" [51,51] 1000)
+  e_const_fst :: Ex => Const
 
-  t_const :: "TyConst => Ty"
-  t_fun :: "[Ty, Ty] => Ty" ("_ -> _" [51,51] 1000)
+  t_const :: TyConst => Ty
+  t_fun :: [Ty, Ty] => Ty ("_ -> _" [51,51] 1000)
 
-  v_const :: "Const => Val"
-  v_clos :: "Clos => Val"
+  v_const :: Const => Val
+  v_clos :: Clos => Val
   
-  ve_emp :: "ValEnv"
-  ve_owr :: "[ValEnv, ExVar, Val] => ValEnv" ("_ + { _ |-> _ }" [36,0,0] 50)
-  ve_dom :: "ValEnv => ExVar set"
-  ve_app :: "[ValEnv, ExVar] => Val"
+  ve_emp :: ValEnv
+  ve_owr :: [ValEnv, ExVar, Val] => ValEnv ("_ + { _ |-> _ }" [36,0,0] 50)
+  ve_dom :: ValEnv => ExVar set
+  ve_app :: [ValEnv, ExVar] => Val
 
-  clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000)
+  clos_mk :: [ExVar, Ex, ValEnv] => Clos ("<| _ , _ , _ |>" [0,0,0] 1000)
 
-  te_emp :: "TyEnv"
-  te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50)
-  te_app :: "[TyEnv, ExVar] => Ty"
-  te_dom :: "TyEnv => ExVar set"
+  te_emp :: TyEnv
+  te_owr :: [TyEnv, ExVar, Ty] => TyEnv ("_ + { _ |=> _ }" [36,0,0] 50)
+  te_app :: [TyEnv, ExVar] => Ty
+  te_dom :: TyEnv => ExVar set
 
   eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
   eval_rel :: "((ValEnv * Ex) * Val) set"
-  eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50)
+  eval :: [ValEnv, Ex, Val] => bool ("_ |- _ ---> _" [36,0,36] 50)
 
   elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
   elab_rel :: "((TyEnv * Ex) * Ty) set"
-  elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
+  elab :: [TyEnv, Ex, Ty] => bool ("_ |- _ ===> _" [36,0,36] 50)
   
-  isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
-  isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
+  isof :: [Const, Ty] => bool ("_ isof _" [36,36] 50)
+  isof_env :: [ValEnv,TyEnv] => bool ("_ isofenv _")
 
   hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
   hasty_rel :: "(Val * Ty) set"
-  hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
-  hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
+  hasty :: [Val, Ty] => bool ("_ hasty _" [36,36] 50)
+  hasty_env :: [ValEnv,TyEnv] => bool ("_ hastyenv _ " [36,36] 35)
 
 rules
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/NatSum.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -7,7 +7,7 @@
 *)
 
 NatSum = Arith +
-consts sum     :: "[nat=>nat, nat] => nat"
+consts sum     :: [nat=>nat, nat] => nat
 rules  sum_0      "sum f 0 = 0"
        sum_Suc    "sum f (Suc n) = f(n) + sum f n"
 end
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/Perm.thy
--- a/src/HOL/ex/Perm.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Perm.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -9,7 +9,7 @@
 Perm = List +
 
 consts  perm    :: "('a list * 'a list) set"   
-syntax "@perm"  :: "['a list, 'a list] => bool" ("_ <~~> _"  [50,50] 50)
+syntax "@perm"  :: ['a list, 'a list] => bool ("_ <~~> _"  [50,50] 50)
 
 translations
     "x <~~> y" == "(x,y) : perm"
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/PropLog.thy
--- a/src/HOL/ex/PropLog.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/PropLog.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -10,12 +10,12 @@
 datatype
     'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
 consts
-  thms :: "'a pl set => 'a pl set"
-  "|-" 	:: "['a pl set, 'a pl] => bool"	(infixl 50)
-  "|="	:: "['a pl set, 'a pl] => bool"	(infixl 50)
-  eval2	:: "['a pl, 'a set] => bool"
-  eval	:: "['a set, 'a pl] => bool"	("_[_]" [100,0] 100)
-  hyps	:: "['a pl, 'a set] => 'a pl set"
+  thms :: 'a pl set => 'a pl set
+  "|-" 	:: ['a pl set, 'a pl] => bool	(infixl 50)
+  "|="	:: ['a pl set, 'a pl] => bool	(infixl 50)
+  eval2	:: ['a pl, 'a set] => bool
+  eval	:: ['a set, 'a pl] => bool	("_[_]" [100,0] 100)
+  hyps	:: ['a pl, 'a set] => 'a pl set
 
 translations
   "H |- p" == "p : thms(H)"
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/Puzzle.thy
--- a/src/HOL/ex/Puzzle.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Puzzle.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -7,6 +7,6 @@
 *)
 
 Puzzle = Nat +
-consts f :: "nat => nat"
+consts f :: nat => nat
 rules  f_ax "f(f(n)) < f(Suc(n))"
 end
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/Qsort.thy
--- a/src/HOL/ex/Qsort.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Qsort.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -8,7 +8,7 @@
 
 Qsort = Sorting +
 consts
-  qsort  :: "[['a,'a] => bool, 'a list] => 'a list"
+  qsort  :: [['a,'a] => bool, 'a list] => 'a list
 
 rules
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/Rec.thy
--- a/src/HOL/ex/Rec.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Rec.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -1,8 +1,8 @@
 Rec = Fixedpt +
 consts
-fix	:: "('a=>'a) => 'a"
-Dom	:: "(('a=>'b) => ('a=>'b)) => 'a set"
-Domf	:: "(('a=>'b) => ('a=>'b)) => 'a set => 'a set"
+fix	:: ('a=>'a) => 'a
+Dom	:: (('a=>'b) => ('a=>'b)) => 'a set
+Domf	:: (('a=>'b) => ('a=>'b)) => 'a set => 'a set
 rules
 Domf_def "Domf(F,D) == {y . !f g. (!x:D. f(x)=g(x)) --> F(f,y)=F(g,y)}"
 Dom_def  "Dom(F) == lfp(Domf(F))"
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/SList.thy
--- a/src/HOL/ex/SList.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/SList.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -21,36 +21,36 @@
 
 consts
 
-  list      :: "'a item set => 'a item set"
-  Rep_list  :: "'a list => 'a item"
-  Abs_list  :: "'a item => 'a list"
-  NIL       :: "'a item"
-  CONS      :: "['a item, 'a item] => 'a item"
-  Nil       :: "'a list"
-  "#"       :: "['a, 'a list] => 'a list"                   	(infixr 65)
-  List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
-  List_rec  :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
-  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
-  list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
-  Rep_map   :: "('b => 'a item) => ('b list => 'a item)"
-  Abs_map   :: "('a item => 'b) => 'a item => 'b list"
-  null      :: "'a list => bool"
-  hd        :: "'a list => 'a"
-  tl,ttl    :: "'a list => 'a list"
-  mem		:: "['a, 'a list] => bool"			(infixl 55)
-  list_all  :: "('a => bool) => ('a list => bool)"
-  map       :: "('a=>'b) => ('a list => 'b list)"
-  "@"	    :: "['a list, 'a list] => 'a list"			(infixr 65)
-  filter    :: "['a => bool, 'a list] => 'a list"
+  list      :: 'a item set => 'a item set
+  Rep_list  :: 'a list => 'a item
+  Abs_list  :: 'a item => 'a list
+  NIL       :: 'a item
+  CONS      :: ['a item, 'a item] => 'a item
+  Nil       :: 'a list
+  "#"       :: ['a, 'a list] => 'a list                   	(infixr 65)
+  List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
+  List_rec  :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
+  list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
+  list_rec  :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
+  Rep_map   :: ('b => 'a item) => ('b list => 'a item)
+  Abs_map   :: ('a item => 'b) => 'a item => 'b list
+  null      :: 'a list => bool
+  hd        :: 'a list => 'a
+  tl,ttl    :: 'a list => 'a list
+  mem		:: ['a, 'a list] => bool			(infixl 55)
+  list_all  :: ('a => bool) => ('a list => bool)
+  map       :: ('a=>'b) => ('a list => 'b list)
+  "@"	    :: ['a list, 'a list] => 'a list			(infixr 65)
+  filter    :: ['a => bool, 'a list] => 'a list
 
   (* list Enumeration *)
 
-  "[]"      :: "'a list"                            ("[]")
-  "@list"   :: "args => 'a list"                    ("[(_)]")
+  "[]"      :: 'a list                            ("[]")
+  "@list"   :: args => 'a list                    ("[(_)]")
 
   (* Special syntax for list_all and filter *)
-  "@Alls"	:: "[idt, 'a list, bool] => bool"	("(2Alls _:_./ _)" 10)
-  "@filter"	:: "[idt, 'a list, bool] => 'a list"	("(1[_:_ ./ _])")
+  "@Alls"	:: [idt, 'a list, bool] => bool	("(2Alls _:_./ _)" 10)
+  "@filter"	:: [idt, 'a list, bool] => 'a list	("(1[_:_ ./ _])")
 
 translations
   "[x, xs]"     == "x#[xs]"
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/Simult.thy
--- a/src/HOL/ex/Simult.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Simult.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -21,16 +21,16 @@
 arities  tree,forest :: (term)term
 
 consts
-  TF          :: "'a item set => 'a item set"
-  FNIL        :: "'a item"
-  TCONS,FCONS :: "['a item, 'a item] => 'a item"
-  Rep_Tree    :: "'a tree => 'a item"
-  Abs_Tree    :: "'a item => 'a tree"
-  Rep_Forest  :: "'a forest => 'a item"
-  Abs_Forest  :: "'a item => 'a forest"
-  Tcons       :: "['a, 'a forest] => 'a tree"
-  Fcons       :: "['a tree, 'a forest] => 'a forest"
-  Fnil        :: "'a forest"
+  TF          :: 'a item set => 'a item set
+  FNIL        :: 'a item
+  TCONS,FCONS :: ['a item, 'a item] => 'a item
+  Rep_Tree    :: 'a tree => 'a item
+  Abs_Tree    :: 'a item => 'a tree
+  Rep_Forest  :: 'a forest => 'a item
+  Abs_Forest  :: 'a item => 'a forest
+  Tcons       :: ['a, 'a forest] => 'a tree
+  Fcons       :: ['a tree, 'a forest] => 'a forest
+  Fnil        :: 'a forest
   TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     
                  'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
   tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,          
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Sorting.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -8,11 +8,11 @@
 
 Sorting = List +
 consts
-  sorted1:: "[['a,'a] => bool, 'a list] => bool"
-  sorted :: "[['a,'a] => bool, 'a list] => bool"
-  mset   :: "'a list => ('a => nat)"
-  total  :: "(['a,'a] => bool) => bool"
-  transf :: "(['a,'a] => bool) => bool"
+  sorted1:: [['a,'a] => bool, 'a list] => bool
+  sorted :: [['a,'a] => bool, 'a list] => bool
+  mset   :: 'a list => ('a => nat)
+  total  :: (['a,'a] => bool) => bool
+  transf :: (['a,'a] => bool) => bool
 
 rules
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/String.thy
--- a/src/HOL/ex/String.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/String.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -17,8 +17,8 @@
   string = "char list"
 
 syntax
-  "_Char"       :: "xstr => char"       ("CHR _")
-  "_String"     :: "xstr => string"     ("_")
+  "_Char"       :: xstr => char       ("CHR _")
+  "_String"     :: xstr => string     ("_")
 
 end
 
diff -r d04af07266e8 -r 92f83b9d17e1 src/HOL/ex/Term.thy
--- a/src/HOL/ex/Term.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Term.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -16,14 +16,14 @@
 arities term :: (term)term
 
 consts
-  term		:: "'a item set => 'a item set"
-  Rep_term	:: "'a term => 'a item"
-  Abs_term	:: "'a item => 'a term"
-  Rep_Tlist	:: "'a term list => 'a item"
-  Abs_Tlist	:: "'a item => 'a term list"
-  App		:: "['a, ('a term)list] => 'a term"
-  Term_rec	:: "['a item, ['a item , 'a item, 'b list]=>'b] => 'b"
-  term_rec	:: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b"
+  term		:: 'a item set => 'a item set
+  Rep_term	:: 'a term => 'a item
+  Abs_term	:: 'a item => 'a term
+  Rep_Tlist	:: 'a term list => 'a item
+  Abs_Tlist	:: 'a item => 'a term list
+  App		:: ['a, ('a term)list] => 'a term
+  Term_rec	:: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
+  term_rec	:: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
 
 inductive "term(A)"
   intrs