Lines Matching defs:current
505 datatype fvinfo = FVI of { current : term HOLset.set,
510 FVI {current = s, is_full = b, left = NONE, right = NONE}
511 fun current (FVI r) = #current r
526 FVI {current = HOLset.union (current fvs, current xvs),
543 FVI {current = safe_delete (current bodyvs, v),
557 FVI {current = HOLset.union (current fvs, current xvs),
567 FVI {current = safe_delete (current bodyvs, v),
594 val currentfvs = current fvi
610 val bodyfvs = current body_fvi
639 val theta' = filtertheta theta (current fvi)