src/HOL/Decision_Procs/commutative_ring_tac.ML
changeset 44121 44adaa6db327
parent 42361 23f352990944
child 46708 b138dee7bed3
     1.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Wed Aug 10 20:12:36 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Wed Aug 10 20:53:43 2011 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) =
     1.5        if Sign.of_sort thy (T, cr_sort) then
     1.6          let
     1.7 -          val fs = OldTerm.term_frees eq;
     1.8 +          val fs = Misc_Legacy.term_frees eq;
     1.9            val cvs = cterm_of thy (HOLogic.mk_list T fs);
    1.10            val clhs = cterm_of thy (reif_polex T fs lhs);
    1.11            val crhs = cterm_of thy (reif_polex T fs rhs);