changeset 44121 | 44adaa6db327 |
parent 44013 | 5cfc1c36ae97 |
child 44890 | 22f665a2e91c |
--- a/src/HOL/Decision_Procs/MIR.thy Wed Aug 10 20:12:36 2011 +0200 +++ b/src/HOL/Decision_Procs/MIR.thy Wed Aug 10 20:53:43 2011 +0200 @@ -5635,7 +5635,7 @@ let val thy = Thm.theory_of_cterm ct; val t = Thm.term_of ct; - val fs = OldTerm.term_frees t; + val fs = Misc_Legacy.term_frees t; 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;