# HG changeset patch
# User haftmann
# Date 1255342759 -7200
# Node ID bd72e72c3ee33b0cb8acae3437ba0cc4045e988b
# Parent  9aa8dfef16ff71c13d689f8edd78c6f21eecb06b
added is_IVar

diff -r 9aa8dfef16ff -r bd72e72c3ee3 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Oct 12 12:19:19 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Oct 12 12:19:19 2009 +0200
@@ -46,6 +46,7 @@
   val split_pat_abs: iterm -> ((iterm * itype) * iterm) option
   val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
   val unfold_const_app: iterm -> (const * iterm list) option
+  val is_IVar: iterm -> bool
   val eta_expand: int -> const * iterm list -> iterm
   val contains_dictvar: iterm -> bool
   val locally_monomorphic: iterm -> bool
@@ -136,6 +137,9 @@
   | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
     (*see also signature*)
 
+fun is_IVar (IVar _) = true
+  | is_IVar _ = false;
+
 val op `$$ = Library.foldl (op `$);
 val op `|==> = Library.foldr (op `|=>);