Index: /trunk/HasCASL/ParseItem.hs
===================================================================
--- /trunk/HasCASL/ParseItem.hs (revision 11328)
+++ /trunk/HasCASL/ParseItem.hs (revision 11877)
@@ -127,29 +127,9 @@
       <|> typeItemList [p] Plain
 
--- | several 'typeArg's
-typeArgs :: AParser st ([TypeArg], [Token])
-typeArgs = do
-    l <- many1 typeArg
-    return (map fst l, concatMap snd l)
-
-pseudoType :: AParser st TypeScheme
-pseudoType = do
-    l <- asKey lamS
-    (ts, pps) <- typeArgs
-    d <- dotT
-    t <- pseudoType
-    let qs = toRange l pps d
-    case t of
-      TypeScheme ts1 gt ps ->
-          return $ TypeScheme (ts ++ ts1) gt $ appRange qs ps
-  <|> do
-    st <- parseType
-    return $ simpleTypeScheme st
-
 pseudoTypeDef :: TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
 pseudoTypeDef t k l = do
     c <- asKey assignS
-    p <- pseudoType
-    return $ AliasType t k p $ catRange $ l ++ [c]
+    p <- parseType
+    return $ AliasType t k (simpleTypeScheme p) $ catRange $ l ++ [c]
 
 -- * parsing datatypes
Index: /trunk/HasCASL/test/Items.hascasl
===================================================================
--- /trunk/HasCASL/test/Items.hascasl (revision 10650)
+++ /trunk/HasCASL/test/Items.hascasl (revision 11877)
@@ -3,5 +3,5 @@
 var {a}: c -> d
 class Monad < Type -> Type
-type a : Monad := \ t . t -> t
+type (a : Monad) t := t -> t
 free type Term ::=  Var Variable | Lam Variable Term | App Term Term
 type WNet={(sys,i,o): T * T * T . i = o }
Index: /trunk/HasCASL/test/Graphs.hascasl
===================================================================
--- /trunk/HasCASL/test/Graphs.hascasl (revision 4967)
+++ /trunk/HasCASL/test/Graphs.hascasl (revision 11877)
@@ -1,6 +1,6 @@
  var S,T : Type
   type Bool;
-       Pred := \ (S: -Type) . S ->? Unit ;
-       Set := \ S:Type . S ->? Unit ;
+       Pred (S: -Type) := S ->? Unit ;
+       Set (S:Type) := S ->? Unit ;
   ops True, False : Bool;
 
@@ -14,5 +14,5 @@
       __disjointUnion__ :  Set S * Set S -> Set (S*Bool);
       inl,inr : S -> S*Bool;
-  forall x,x':S; y:T; s,s':Set(S); t:Set(T) 
+  forall x,x':S; y:T; s,s':Set(S); t:Set(T)
   . not (x isIn emptySet)
   . (x isIn {x'}) <=> x=x'
Index: /trunk/HasCASL/test/ContraVariance.hascasl.output
===================================================================
--- /trunk/HasCASL/test/ContraVariance.hascasl.output (revision 9230)
+++ /trunk/HasCASL/test/ContraVariance.hascasl.output (revision 11877)
@@ -1,2 +1,3 @@
+var   a : +Type
 type  p a := Pred (Pred a)
       %% should be correct
@@ -9,8 +10,11 @@
 m := \ b : -Type . b;
 p := \ a : +Type . Pred (Pred a)
-### Hint 2.32, wrong covariance of 'a'
-### Hint 2.32, no kind found for 'a'
-*** Error 2.27-2.32, no kind found for 'Pred a'
-*** Error 4.6,
+var
+a : +Type %(var_1)%
+### Hint 1.5, is type variable 'a'
+### Hint 3.18, wrong covariance of 'a'
+### Hint 3.18, no kind found for 'a'
+*** Error 3.13-3.18, no kind found for 'Pred a'
+*** Error 5.6,
 wrong type of 'm'
   expected: \ b : -Type . b
Index: /trunk/HasCASL/test/Graphs.hascasl.output
===================================================================
--- /trunk/HasCASL/test/Graphs.hascasl.output (revision 10502)
+++ /trunk/HasCASL/test/Graphs.hascasl.output (revision 11877)
@@ -70,7 +70,7 @@
 ### Hint 1.6, is type variable 'S'
 ### Hint 1.8, is type variable 'T'
-### Hint 3.19, rebound type variable 'S'
+### Hint 3.14, rebound type variable 'S'
 ### Hint 3.8, redeclared type 'Pred'
-### Hint 4.17, rebound type variable 'S'
+### Hint 4.13, rebound type variable 'S'
 ### Hint 9.18,
 no kind found for 'S'
Index: /trunk/HasCASL/test/Alias.hascasl
===================================================================
--- /trunk/HasCASL/test/Alias.hascasl (revision 8578)
+++ /trunk/HasCASL/test/Alias.hascasl (revision 11877)
@@ -6,10 +6,9 @@
 
 type a1 a b := a -> b -> Unit
-type a1 := \ (a) (b) .a -> b  -> Unit
-type a1 a := \ b .a -> b  -> Unit
+type a1 (a) (b) := a -> b  -> Unit
 
-type a2 := \ (a) (b) . a -> Unit
+type a2 a b := a -> Unit
 
-type a3 := \ (a) (a) . a -> Unit
+type a3 (a) (a) := a -> Unit
 
 type a4 a a := a -> Unit
Index: /trunk/HasCASL/test/Items.hascasl.output
===================================================================
--- /trunk/HasCASL/test/Items.hascasl.output (revision 7441)
+++ /trunk/HasCASL/test/Items.hascasl.output (revision 11877)
@@ -3,5 +3,5 @@
 var   {a} : c -> d
 class Monad < Type -> Type
-type  a t := t -> t
+type  (a : Monad) t := t -> t
 free type Term ::= Var Variable | Lam Variable Term | App Term Term
 type  WNet = {(sys, i, o) : T * T * T . i = o}
Index: /trunk/HasCASL/test/ContraVariance.hascasl
===================================================================
--- /trunk/HasCASL/test/ContraVariance.hascasl (revision 8098)
+++ /trunk/HasCASL/test/ContraVariance.hascasl (revision 11877)
@@ -1,4 +1,5 @@
-type p := \ (a : +Type) . Pred (Pred a)  %% should be correct
-type p := \ (a : +Type) . Pred a         %% should be wrong
-type m := \ (b : -Type) . b              %% 
-type m := \ (b : +Type) . b              %% both contradict
+var a : +Type
+type p a := Pred (Pred a)  %% should be correct
+type p a := Pred a         %% should be wrong
+type m (b : -Type) := b              %%
+type m (b : +Type) := b              %% both contradict
Index: /trunk/HasCASL/test/WrongItems.hascasl.output
===================================================================
--- /trunk/HasCASL/test/WrongItems.hascasl.output (revision 10262)
+++ /trunk/HasCASL/test/WrongItems.hascasl.output (revision 11877)
@@ -11,7 +11,7 @@
 expecting "[", "%", "->", "{", ";", "sort", "op", "fun", "pred", "type", class, "program", "generated", "free", "var", "forall", dot, "axiom", "internal" or end of input
 
-parse error at 4.17:
+parse error at 4.12:
 unexpected list of type arguments
-expecting "%", "+", "-", ",", ":" or "<"
+expecting casl char, "_", "%", "+", "-", ",", ":" or "<"
 
 parse error at 5.12:
Index: /trunk/HasCASL/test/Alias.hascasl.output
===================================================================
--- /trunk/HasCASL/test/Alias.hascasl.output (revision 10502)
+++ /trunk/HasCASL/test/Alias.hascasl.output (revision 11877)
@@ -4,5 +4,4 @@
 type  MyPred s := s ->? Unit
 type  MyAlias t := t ->? Unit
-type  a1 a b := a -> b -> Unit
 type  a1 a b := a -> b -> Unit
 type  a1 a b := a -> b -> Unit
@@ -49,25 +48,22 @@
 *** Error 7.9, unknown type variable 'a'
 *** Error 7.11, unknown type variable 'b'
-*** Error 8.15, unknown type variable 'a'
-*** Error 8.19, unknown type variable 'b'
+*** Error 8.10, unknown type variable 'a'
+*** Error 8.14, unknown type variable 'b'
 ### Hint 8.6, redeclared type 'a1'
-*** Error 9.9, unknown type variable 'a'
-*** Error 9.16, unknown type variable 'b'
-### Hint 9.6, redeclared type 'a1'
-*** Error 11.15, unknown type variable 'a'
-*** Error 11.19, unknown type variable 'b'
-*** Error 13.15, unknown type variable 'a'
-*** Error 13.15, duplicates at '(13,19)' for 'a'
-*** Error 15.9, unknown type variable 'a'
-*** Error 15.9, duplicates at '(15,11)' for 'a'
-*** Error 17.9, unknown type variable 'a'
-*** Error 19.9, unknown type variable 'a'
-*** Error 19.14-19.22,
+*** Error 10.9, unknown type variable 'a'
+*** Error 10.11, unknown type variable 'b'
+*** Error 12.10, unknown type variable 'a'
+*** Error 12.10, duplicates at '(12,14)' for 'a'
+*** Error 14.9, unknown type variable 'a'
+*** Error 14.9, duplicates at '(14,11)' for 'a'
+*** Error 16.9, unknown type variable 'a'
+*** Error 18.9, unknown type variable 'a'
+*** Error 18.14-18.22,
 illegal recursive type synonym 'a5 a -> Unit'
-*** Error 21.9, unknown type variable 'a'
-*** Error 23.9, unknown type variable 'a'
-*** Error 25.9, unknown type variable 'a'
-*** Error 23.9-25.22, illegal recursive type synonym 'a7 a -> Unit'
-*** Error 27.6,
+*** Error 20.9, unknown type variable 'a'
+*** Error 22.9, unknown type variable 'a'
+*** Error 24.9, unknown type variable 'a'
+*** Error 22.9-24.22, illegal recursive type synonym 'a7 a -> Unit'
+*** Error 26.6,
 incompatible kind of: a2
   expected: Type -> Type -> Type
Index: /trunk/HasCASL/test/WrongItems.hascasl
===================================================================
--- /trunk/HasCASL/test/WrongItems.hascasl (revision 10262)
+++ /trunk/HasCASL/test/WrongItems.hascasl (revision 11877)
@@ -2,4 +2,4 @@
 var <
 class a < Type = {x . x < t}
-type t := \ s,r . s -> r
+type t (s,r) := s -> r
 type n (r,s)
Index: /trunk/HasCASL/test/Prelude.hascasl
===================================================================
--- /trunk/HasCASL/test/Prelude.hascasl (revision 4544)
+++ /trunk/HasCASL/test/Prelude.hascasl (revision 11877)
@@ -1,8 +1,8 @@
-%% predefined universe containing all types, 
+%% predefined universe containing all types,
 %% superclass of all other classes
 
 class Type
 
-var s,t  : Type 
+var s,t  : Type
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -12,6 +12,6 @@
 
 %% type aliases
-type Pred __ : Type -> Type := \ t: -Type . t ->? Unit 
-type ? __ := \ t:Type . Unit ->? t
+type Pred __ (t: -Type) := t ->? Unit
+type ? __ (t:Type) := Unit ->? t
 
 pred true, false : Unit
@@ -34,5 +34,5 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% "pred p args = e" abbreviates "op p args :? unit = e"  
+%% "pred p args = e" abbreviates "op p args :? unit = e"
 %% CASL requires "<=>" for pred-defn and disallows "()" as result
 
@@ -40,5 +40,5 @@
 var x : s
 
-program def = \x: s . () %% def is also total (identical to tt) 
+program def = \x: s . () %% def is also total (identical to tt)
 
 program tt = \x: s . ()  %% tt is total "op tt(x: s): unit = ()"
@@ -48,5 +48,5 @@
 
 %% total function type
-type __->__ : -Type -> +Type -> Type 
+type __->__ : -Type -> +Type -> Type
 
 type __->__ < __ ->? __
@@ -56,12 +56,12 @@
 
 %% total functions
-op __res__ (x: s; y: t) : s = x 
-op fst (x: s; y: t) : s = x 
-program snd (x: s, y: t) : t = y 
+op __res__ (x: s; y: t) : s = x
+op fst (x: s; y: t) : s = x
+program snd (x: s, y: t) : t = y
 
 
 %% trivial because its the strict function property
 
-. (\ (x:s, y:t). def (x res y)) =  (\ (x:s, y:t). (def y) und (def x)) 
+. (\ (x:s, y:t). def (x res y)) =  (\ (x:s, y:t). (def y) und (def x))
 . fst = (__ res__)
 
@@ -77,8 +77,8 @@
 %% then %def
 
-%% notation "\ ."  abbreviates "\bla:unit." 
+%% notation "\ ."  abbreviates "\bla:unit."
 %% where "bla" is never used, but only "()" instead
 
-%% for type inference 
+%% for type inference
 %% an implicit cast from s to ?s of a term "e" yields the term "\ . e"
 
@@ -93,5 +93,5 @@
 program __impl__ (x, y: Pred Unit) : Pred Unit = eq(x, x And y)
 
-program __or__ (x, y: Pred Unit) : Pred Unit = all(\r: Pred Unit. 
+program __or__ (x, y: Pred Unit) : Pred Unit = all(\r: Pred Unit.
 		((x impl r) und (y impl r)) impl r)
 
@@ -103,5 +103,5 @@
 program neg (r: Pred Unit) : Pred Unit = r impl ff
 
-%% the type instance for the first "eq" should be "?t" 
+%% the type instance for the first "eq" should be "?t"
 %% this is explicitely enforced by "\ .f(x)"
 
@@ -109,5 +109,5 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"  
+%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"
 
 type nat
@@ -124,5 +124,5 @@
 
 pred isChain (s: nat -> c) <=> all(\n:nat. s(n) <<= s(Suc(n)))
-pred isBound (x: c; s: nat -> c) <=> all(\n:nat. s(n) <<= x)  
+pred isBound (x: c; s: nat -> c) <=> all(\n:nat. s(n) <<= x)
 
 op sup : (nat -> c) ->? c
@@ -139,12 +139,12 @@
 var p : Pcpo
 
-op bottom : p 
-
-. all(\x : p. bottom <<= x)   
+op bottom : p
+
+. all(\x : p. bottom <<= x)
 }
 
 class instance Flatcpo < Cpo
 {
- var f : Flatcpo 
+ var f : Flatcpo
 
  program __<<=[f]__ = eq
@@ -155,21 +155,21 @@
 type instance __*__ : +Cpo -> +Cpo -> Cpo
 
-var x1,x2 : c; y1, y2 : d 
-
-program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2) 
-
-
-type instance __*__ : +Pcpo -> +Pcpo -> Pcpo      
+var x1,x2 : c; y1, y2 : d
+
+program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2)
+
+
+type instance __*__ : +Pcpo -> +Pcpo -> Pcpo
 
 type Unit : Pcpo
 
 %% Pcont
-type instance __-->?__ : -Cpo -> +Cpo -> Pcpo 
+type instance __-->?__ : -Cpo -> +Cpo -> Pcpo
 
  type __-->?__ < __->?__
- . __ in c -->? d  = \f : c ->? d . 
+ . __ in c -->? d  = \f : c ->? d .
 	all(\(x,y: c). (def (f x) und x <<= y) impl def (f y)) und
-	all(\s: nat -> c. (isChain(s) und def f(sup(s))) impl 
-		ex(\m:nat. def f(s(m)) und 
+	all(\s: nat -> c. (isChain(s) und def f(sup(s))) impl
+		ex(\m:nat. def f(s(m)) und
 			eq(sup(\n:nat.!f(s(n+m))), f(sup(s)))))
 
@@ -179,10 +179,10 @@
 type instance __-->__ : -Cpo -> +Cpo -> Cpo
 
- type __-->__ < __-->?__ 
+ type __-->__ < __-->?__
  . __ in c --> d = \f : c -->? d . all(\x:c. def f(x))
 
  var f, g : c --> d
 
- program f <<= g = f <<=[c -->? d] g 
+ program f <<= g = f <<=[c -->? d] g
 
 type instance __-->__ : -Cpo -> +Pcpo -> Pcpo
@@ -195,5 +195,5 @@
 var f : p --> p; x : p
 . f(Y(f)) = Y(f)
-. f(x) = x => Y(f) <<= x  
+. f(x) = x => Y(f) <<= x
 
 op undefined : c --> p = Y((\x': c --> p . x') as (c --> p) --> c --> p)