src/HOL/Tools/TFL/casesplit.ML

 (*  Title:      HOL/Tools/TFL/casesplit.ML
-    ID:         $Id$
     Author:     Lucas Dixon, University of Edinburgh
 
 A structure that defines a tactic to program case splits.
 
     casesplit_free :

     in
       cases_thm_of_induct_thm (#induction dt)
     end;
 
 (*
- val ty = (snd o hd o map Term.dest_Free o Term.term_frees) t;
+ val ty = (snd o hd o map Term.dest_Free o OldTerm.term_frees) t;
 *)
 
 
 (* for use when there are no prems to the subgoal *)
 (* does a case split on the given variable *)

       val case_thm = case_thm_of_ty sgn ty;
 
       val abs_ct = ctermify abst;
       val free_ct = ctermify x;
 
-      val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm));
+      val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
 
       val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
       val (Pv, Dv, type_insts) =
           case (Thm.concl_of case_thm) of
             (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>

     let
       val (subgoalth, exp) = IsaND.fix_alls i th;
       val subgoalth' = atomize_goals subgoalth;
       val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
 
-      val freets = Term.term_frees gt;
+      val freets = OldTerm.term_frees gt;
       fun getter x =
           let val (n,ty) = Term.dest_Free x in
             (if vstr = n orelse vstr = Name.dest_skolem n
              then SOME (n,ty) else NONE )
             handle Fail _ => NONE (* dest_skolem *)