TFL/post.ML
changeset 16287 7a03b4b4df67
parent 15574 b1d1b5bfc464
child 16852 b950180e243d
equal deleted inserted replaced
16286:550d113ccd8f 16287:7a03b4b4df67
    43 (*---------------------------------------------------------------------------
    43 (*---------------------------------------------------------------------------
    44  * Extract termination goals so that they can be put it into a goalstack, or
    44  * Extract termination goals so that they can be put it into a goalstack, or
    45  * have a tactic directly applied to them.
    45  * have a tactic directly applied to them.
    46  *--------------------------------------------------------------------------*)
    46  *--------------------------------------------------------------------------*)
    47 fun termination_goals rules =
    47 fun termination_goals rules =
    48     map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
    48     map (Type.freeze o HOLogic.dest_Trueprop)
    49       (foldr (fn (th,A) => union_term (prems_of th, A)) [] rules);
    49       (foldr (fn (th,A) => union_term (prems_of th, A)) [] rules);
    50 
    50 
    51 (*---------------------------------------------------------------------------
    51 (*---------------------------------------------------------------------------
    52  * Finds the termination conditions in (highly massaged) definition and
    52  * Finds the termination conditions in (highly massaged) definition and
    53  * puts them into a goalstack.
    53  * puts them into a goalstack.