TFL/post.ML
changeset 12341 08afd1003151
parent 11771 b7b100a2de1d
child 12488 83acab8042ad
equal deleted inserted replaced
12340:24d31d47af1a 12341:08afd1003151
    35 fun message s = if ! quiet_mode then () else writeln s;
    35 fun message s = if ! quiet_mode then () else writeln s;
    36 
    36 
    37 
    37 
    38 (* misc *)
    38 (* misc *)
    39 
    39 
    40 fun read_term thy = Sign.simple_read_term (Theory.sign_of thy) HOLogic.termT;
    40 val read_term = Thm.term_of oo (HOLogic.read_cterm o Theory.sign_of);
    41 
    41 
    42 
    42 
    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.