added is_IVar
authorhaftmann
Mon Oct 12 12:19:19 2009 +0200 (2009-10-12)
changeset 32909bd72e72c3ee3
parent 32908 9aa8dfef16ff
child 32910 d61e303fc7e5
added is_IVar
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Oct 12 12:19:19 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Oct 12 12:19:19 2009 +0200
     1.3 @@ -46,6 +46,7 @@
     1.4    val split_pat_abs: iterm -> ((iterm * itype) * iterm) option
     1.5    val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
     1.6    val unfold_const_app: iterm -> (const * iterm list) option
     1.7 +  val is_IVar: iterm -> bool
     1.8    val eta_expand: int -> const * iterm list -> iterm
     1.9    val contains_dictvar: iterm -> bool
    1.10    val locally_monomorphic: iterm -> bool
    1.11 @@ -136,6 +137,9 @@
    1.12    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
    1.13      (*see also signature*)
    1.14  
    1.15 +fun is_IVar (IVar _) = true
    1.16 +  | is_IVar _ = false;
    1.17 +
    1.18  val op `$$ = Library.foldl (op `$);
    1.19  val op `|==> = Library.foldr (op `|=>);
    1.20