equal
deleted
inserted
replaced
1994 |
1994 |
1995 in fn ct => |
1995 in fn ct => |
1996 let |
1996 let |
1997 val thy = Thm.theory_of_cterm ct; |
1997 val thy = Thm.theory_of_cterm ct; |
1998 val t = Thm.term_of ct; |
1998 val t = Thm.term_of ct; |
1999 val fs = OldTerm.term_frees t; |
1999 val fs = Misc_Legacy.term_frees t; |
2000 val bs = term_bools [] t; |
2000 val bs = term_bools [] t; |
2001 val vs = map_index swap fs; |
2001 val vs = map_index swap fs; |
2002 val ps = map_index swap bs; |
2002 val ps = map_index swap bs; |
2003 val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t; |
2003 val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t; |
2004 in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end |
2004 in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end |