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