src/HOL/Decision_Procs/cooper_tac.ML
changeset 44121 44adaa6db327
parent 43594 ef1ddc59b825
child 45620 f2a587696afb
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Wed Aug 10 20:12:36 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Aug 10 20:53:43 2011 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4      val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
     1.5        (List.foldr HOLogic.mk_imp c rhs, np) ps
     1.6      val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
     1.7 -      (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
     1.8 +      (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
     1.9      val fm2 = List.foldr mk_all2 fm' vs
    1.10    in (fm2, np + length vs, length rhs) end;
    1.11