equal
deleted
inserted
replaced
2647 val fs = Misc_Legacy.term_frees t; |
2647 val fs = Misc_Legacy.term_frees t; |
2648 val bs = term_bools [] t; |
2648 val bs = term_bools [] t; |
2649 val vs = map_index swap fs; |
2649 val vs = map_index swap fs; |
2650 val ps = map_index swap bs; |
2650 val ps = map_index swap bs; |
2651 val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t; |
2651 val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t; |
2652 in Thm.cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end |
2652 in Thm.global_cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end |
2653 end; |
2653 end; |
2654 *} |
2654 *} |
2655 |
2655 |
2656 ML_file "cooper_tac.ML" |
2656 ML_file "cooper_tac.ML" |
2657 |
2657 |