1.1 --- a/src/Tools/Code/code_thingol.ML	Thu Feb 17 09:31:29 2011 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Feb 17 09:31:29 2011 +0100
     1.3 @@ -15,14 +15,15 @@
     1.4  sig
     1.5    type vname = string;
     1.6    datatype dict =
     1.7 -      Dict of (string list * plain_dict)
     1.8 +      Dict of string list * plain_dict
     1.9    and plain_dict = 
    1.10        Dict_Const of string * dict list list
    1.11      | Dict_Var of vname * (int * int)
    1.12    datatype itype =
    1.13        `%% of string * itype list
    1.14      | ITyVar of vname;
    1.15 -  type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
    1.16 +  type const = string * ((itype list * dict list list) * itype list)
    1.17 +    (* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *)
    1.18    datatype iterm =
    1.19        IConst of const
    1.20      | IVar of vname option
    1.21 @@ -51,6 +52,7 @@
    1.22    val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
    1.23    val unfold_const_app: iterm -> (const * iterm list) option
    1.24    val is_IVar: iterm -> bool
    1.25 +  val is_IAbs: iterm -> bool
    1.26    val eta_expand: int -> const * iterm list -> iterm
    1.27    val contains_dict_var: iterm -> bool
    1.28    val locally_monomorphic: iterm -> bool
    1.29 @@ -134,7 +136,7 @@
    1.30  type vname = string;
    1.31  
    1.32  datatype dict =
    1.33 -    Dict of (string list * plain_dict)
    1.34 +    Dict of string list * plain_dict
    1.35  and plain_dict = 
    1.36      Dict_Const of string * dict list list
    1.37    | Dict_Var of vname * (int * int)
    1.38 @@ -156,6 +158,9 @@
    1.39  fun is_IVar (IVar _) = true
    1.40    | is_IVar _ = false;
    1.41  
    1.42 +fun is_IAbs (_ `|=> _) = true
    1.43 +  | is_IAbs _ = false;
    1.44 +
    1.45  val op `$$ = Library.foldl (op `$);
    1.46  val op `|==> = Library.foldr (op `|=>);
    1.47