--- 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 `|=>);