src/HOL/Tools/choice_specification.ML

 
 (* actual code *)
 
 fun close_form t =
     fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t))
-             (map dest_Free (OldTerm.term_frees t)) t
+             (map dest_Free (Misc_Legacy.term_frees t)) t
 
 local
     fun mk_definitional [] arg = arg
       | mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
         case HOLogic.dest_Trueprop (concl_of thm) of

         val props' = rew_imps |>
           map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
 
         fun proc_single prop =
             let
-                val frees = OldTerm.term_frees prop
+                val frees = Misc_Legacy.term_frees prop
                 val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
                   orelse error "Specificaton: Only free variables of sort 'type' allowed"
                 val prop_closed = close_form prop
             in
                 (prop_closed,frees)