equal
deleted
inserted
replaced
5653 val t = Thm.term_of ct; |
5653 val t = Thm.term_of ct; |
5654 val fs = Misc_Legacy.term_frees t; |
5654 val fs = Misc_Legacy.term_frees t; |
5655 val vs = map_index swap fs; |
5655 val vs = map_index swap fs; |
5656 val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe}; |
5656 val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe}; |
5657 val t' = (term_of_fm vs o qe o fm_of_term vs) t; |
5657 val t' = (term_of_fm vs o qe o fm_of_term vs) t; |
5658 in (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end |
5658 in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end |
5659 end; |
5659 end; |
5660 *} |
5660 *} |
5661 |
5661 |
5662 ML_file "mir_tac.ML" |
5662 ML_file "mir_tac.ML" |
5663 |
5663 |