changeset 33063 | 4d462963a7db |
parent 32960 | 69916a850301 |
child 33639 | 603320b93668 |
--- a/src/HOL/Decision_Procs/MIR.thy Thu Oct 22 10:52:07 2009 +0200 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Oct 22 13:48:06 2009 +0200 @@ -5898,7 +5898,7 @@ val thy = Thm.theory_of_cterm ct; val t = Thm.term_of ct; val fs = OldTerm.term_frees t; - val vs = fs ~~ (0 upto (length fs - 1)); + val vs = map_index swap fs; val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe}; val t' = (term_of_fm vs o qe o fm_of_term vs) t; in (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end